From 33d7804d6a2eb3e7c9e2017d1caeedeae5e4a5cb Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Jan 2010 13:35:28 +0000
Subject: Numbers: two more Local Obligation Tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12652 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Integer/SpecViaZ')

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index cb5a771daa..a94e1a318f 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -38,7 +38,7 @@ Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 Instance eq_equiv : Equivalence Z.eq.
 Proof. unfold Z.eq. firstorder. Qed.
 
-Obligation Tactic := zcongruence.
+Local Obligation Tactic := zcongruence.
 
 Program Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ.
 Program Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred.
-- 
cgit v1.2.3