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