From bc1168a4aa0a336e9686b57cc29ec562aa379973 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 18 Dec 2009 15:27:45 +0000 Subject: RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd As a consequence, revert to some pedestrian proofs of Equivalence here and there, without the need for the Measure class. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v') diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index aa291cfdc..66d3a89c2 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -34,9 +34,8 @@ Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence. Obligation Tactic := ncongruence. -Instance: @Measure N.t Z N.to_Z. - Instance eq_equiv : Equivalence N.eq. +Proof. unfold N.eq. firstorder. Qed. Program Instance succ_wd : Proper (N.eq==>N.eq) N.succ. Program Instance pred_wd : Proper (N.eq==>N.eq) N.pred. -- cgit v1.2.3