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

7 files changed, 9 insertions, 7 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index da33059c95..e3c14879df 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -61,8 +61,10 @@ Ltac wsimpl :=
  unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w.
 Ltac wcongruence := repeat red; intros; wsimpl; congruence.
 
-Instance znz_measure: Measure w_op.(znz_to_Z).
 Instance eq_equiv : Equivalence eq.
+Proof.
+unfold eq. firstorder.
+Qed.
 
 Instance succ_wd : Proper (eq ==> eq) succ.
 Proof.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 0d8f8bf5d4..516827616f 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -12,7 +12,7 @@
 
 
 Require Import ZAxioms ZProperties.
-Require Import ZArith.
+Require Import ZArith_base.
 
 Local Open Scope Z_scope.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 410af329db..f752c19761 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -36,8 +36,8 @@ Hint Rewrite
 Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec.
 Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 
-Instance Z_measure: @Measure Z.t Z Z.to_Z.
 Instance eq_equiv : Equivalence Z.eq.
+Proof. unfold Z.eq. firstorder. Qed.
 
 Obligation Tactic := zcongruence.
 
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 1239173752..69dbf656e3 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -11,6 +11,7 @@
 (*i $Id$ i*)
 
 Require Import Bool. (* To get the orb and negb function *)
+Require Import RelationPairs.
 Require Export NStrongRec.
 
 Module NdefOpsPropFunct (Import N : NAxiomsSig).
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index aa291cfdce..66d3a89c29 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.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 290c9b1c2c..32860cd31e 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -10,7 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Export Setoid Morphisms RelationPairs.
+Require Export Setoid Morphisms.
 
 Set Implicit Arguments.
 (*
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 14646fa84a..fcfb5d7e75 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -94,8 +94,8 @@ Local Open Scope bigQ_scope.
 
 (** [BigQ] is a setoid *)
 
-Instance bigQ_measure: RelationPairs.Measure BigQ.to_Q.
 Instance BigQeq_rel : Equivalence BigQ.eq.
+Proof. unfold BigQ.eq. split; red; eauto with qarith. Qed.
 
 Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add.
 Proof.