diff options
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 | ||||
| -rw-r--r-- | 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 cb5a771da..a94e1a318 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 8a34185d9..0e3be25aa 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. |