diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |