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/Natural/SpecViaZ/NSigNAxioms.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Natural')

diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 8a34185d94..0e3be25aaf 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -30,7 +30,7 @@ Hint Rewrite
 Ltac nsimpl := autorewrite with num.
 Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence.
 
-Obligation Tactic := ncongruence.
+Local Obligation Tactic := ncongruence.
 
 Instance eq_equiv : Equivalence N.eq.
 Proof. unfold N.eq. firstorder. Qed.
-- 
cgit v1.2.3