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 +-
 theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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.
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