Numbers: more (syntactic) changes toward new style of type classes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7

20 files changed, 181 insertions, 459 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index c6532d868..2076a9ab2 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -45,29 +45,29 @@ Definition NZmul := w_op.(znz_mul).
 
 Instance NZeq_equiv : Equivalence NZeq.
 
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
+Instance NZsucc_wd : Proper (NZeq ==> NZeq) NZsucc.
 Proof.
 unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
+Instance NZpred_wd : Proper (NZeq ==> NZeq) NZpred.
 Proof.
 unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
 Qed.
 
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
+Instance NZadd_wd : Proper (NZeq ==> NZeq ==> NZeq) NZadd.
 Proof.
 unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
+Instance NZsub_wd : Proper (NZeq ==> NZeq ==> NZeq) NZsub.
 Proof.
 unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
+Instance NZmul_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmul.
 Proof.
 unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
 now rewrite H1, H2.
@@ -135,13 +135,10 @@ Qed.
 Section Induction.
 
 Variable A : NZ -> Prop.
-Hypothesis A_wd : predicate_wd NZeq A.
+Hypothesis A_wd : Proper (NZeq ==> iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
 
-Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
-
 Let B (n : Z) := A (Z_to_NZ n).
 
 Lemma B0 : B 0.
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 917e3fc12..5f68b2bb1 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -350,9 +350,7 @@ Qed.
 Section PosNeg.
 
 Variable P : Z -> Prop.
-Hypothesis P_wd : predicate_wd Zeq P.
-
-Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed.
+Hypothesis P_wd : Proper (Zeq ==> iff) P.
 
 Theorem Z0_pos_neg :
   P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 7b3c0ba6e..00e34a5b5 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -64,7 +64,7 @@ Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
 Proof NZeq_dne.
 
 Theorem Zcentral_induction :
-forall A : Z -> Prop, predicate_wd Zeq A ->
+forall A : Z -> Prop, Proper (Zeq==>iff) A ->
   forall z : Z, A z ->
     (forall n : Z, A n <-> A (S n)) ->
       forall n : Z, A n.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 4d927cb3b..500dd9f53 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -10,22 +10,17 @@
 
 (*i $Id$ i*)
 
+Require Import Bool.
 Require Export NumPrelude.
 
 Module Type ZDomainSignature.
 
 Parameter Inline Z : Set.
 Parameter Inline Zeq : Z -> Z -> Prop.
-Parameter Inline e : Z -> Z -> bool.
+Parameter Inline Zeqb : Z -> Z -> bool.
 
-Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
-Axiom eq_equiv : equiv Z Zeq.
-
-Add Relation Z Zeq
- reflexivity proved by (proj1 eq_equiv)
- symmetry proved by (proj2 (proj2 eq_equiv))
- transitivity proved by (proj1 (proj2 eq_equiv))
-as eq_rel.
+Axiom eqb_equiv_eq : forall x y : Z, Zeqb x y = true <-> Zeq x y.
+Instance eq_equiv : Equivalence Zeq.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
@@ -37,16 +32,11 @@ End ZDomainSignature.
 Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
 Open Local Scope IntScope.
 
-Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
+Instance Zeqb_wd : Proper (Zeq ==> Zeq ==> eq) Zeqb.
 Proof.
 intros x x' Exx' y y' Eyy'.
-case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
-assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
-assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
+apply eq_true_iff_eq.
+rewrite 2 eqb_equiv_eq, Exx', Eyy'; auto with *.
 Qed.
 
 Theorem neq_sym : forall n m, n # m -> m # n.
@@ -62,7 +52,7 @@ Qed.
 Declare Left Step ZE_stepl.
 
 (* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (proj1 (proj2 eq_equiv)).
+Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
 
 End ZDomainProperties.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 1b8bdda40..efd1f0da3 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -221,21 +221,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem Zright_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
         forall n : Z, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem Zleft_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem Zright_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
@@ -243,7 +243,7 @@ Theorem Zright_induction' :
 Proof NZright_induction'.
 
 Theorem Zleft_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -251,21 +251,21 @@ Theorem Zleft_induction' :
 Proof NZleft_induction'.
 
 Theorem Zstrong_right_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
        forall n : Z, z <= n -> A n.
 Proof NZstrong_right_induction.
 
 Theorem Zstrong_left_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZstrong_left_induction.
 
 Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
@@ -273,7 +273,7 @@ Theorem Zstrong_right_induction' :
 Proof NZstrong_right_induction'.
 
 Theorem Zstrong_left_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
@@ -281,7 +281,7 @@ Theorem Zstrong_left_induction' :
 Proof NZstrong_left_induction'.
 
 Theorem Zorder_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
     (forall n : Z, z <= n -> A n -> A (S n)) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -289,7 +289,7 @@ Theorem Zorder_induction :
 Proof NZorder_induction.
 
 Theorem Zorder_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
     (forall n : Z, z <= n -> A n -> A (S n)) ->
     (forall n : Z, n <= z -> A n -> A (P n)) ->
@@ -297,7 +297,7 @@ Theorem Zorder_induction' :
 Proof NZorder_induction'.
 
 Theorem Zorder_induction_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     A 0 ->
     (forall n : Z, 0 <= n -> A n -> A (S n)) ->
     (forall n : Z, n < 0 -> A (S n) -> A n) ->
@@ -305,7 +305,7 @@ Theorem Zorder_induction_0 :
 Proof NZorder_induction_0.
 
 Theorem Zorder_induction'_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     A 0 ->
     (forall n : Z, 0 <= n -> A n -> A (S n)) ->
     (forall n : Z, n <= 0 -> A n -> A (P n)) ->
@@ -317,7 +317,7 @@ Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
 (** Elimintation principle for < *)
 
 Theorem Zlt_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall n : Z, A (S n) ->
       (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
 Proof NZlt_ind.
@@ -325,7 +325,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem Zle_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall n : Z, A n ->
       (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
 Proof NZle_ind.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 7afa1e442..9b55c771c 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -29,31 +29,11 @@ Definition NZsub := Zminus.
 Definition NZmul := Zmult.
 
 Instance NZeq_equiv : Equivalence NZeq.
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc.
+Program Instance NZpred_wd : Proper (eq==>eq) NZpred.
+Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd.
+Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub.
+Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul.
 
 Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n.
 Proof.
@@ -61,7 +41,7 @@ exact Zpred'_succ'.
 Qed.
 
 Theorem NZinduction :
-  forall A : Z -> Prop, predicate_wd NZeq A ->
+  forall A : Z -> Prop, Proper (NZeq ==> iff) A ->
     A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n.
 Proof.
 intros A A_wd A0 AS n; apply Zind; clear n.
@@ -108,25 +88,10 @@ Definition NZle := Zle.
 Definition NZmin := Zmin.
 Definition NZmax := Zmax.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt.
+Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle.
+Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin.
+Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax.
 
 Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n = m.
 Proof.
@@ -182,10 +147,7 @@ match x with
 | Zneg x => Zpos x
 end.
 
-Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd.
-Proof.
-congruence.
-Qed.
+Program Instance Zopp_wd : Proper (eq==>eq) Zopp.
 
 Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 3eb5238d9..dcda3f1e5 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -44,7 +44,7 @@ Qed.
 
 Add Ring NSR : Nsemi_ring.
 
-(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by
+(* The definitions of functions (NZadd, NZmul, etc.) will be unfolded by
 the properties functor. Since we don't want Zadd_comm to refer to unfolded
 definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
 we will provide an extra layer of definitions. *)
@@ -130,24 +130,24 @@ Proof.
 split; [apply ZE_refl | apply ZE_sym | apply ZE_trans].
 Qed.
 
-Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
+Instance Zpair_wd : Proper (NE==>NE==>Zeq) (@pair N N).
 Proof.
 intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
+Instance NZsucc_wd : Proper (Zeq ==> Zeq) NZsucc.
 Proof.
 unfold NZsucc, Zeq; intros n m H; simpl.
 do 2 rewrite add_succ_l; now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
+Instance NZpred_wd : Proper (Zeq ==> Zeq) NZpred.
 Proof.
 unfold NZpred, Zeq; intros n m H; simpl.
 do 2 rewrite add_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd.
+Instance NZadd_wd : Proper (Zeq ==> Zeq ==> Zeq) NZadd.
 Proof.
 unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
@@ -156,7 +156,7 @@ stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
 
-Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd.
+Instance NZsub_wd : Proper (Zeq ==> Zeq ==> Zeq) NZsub.
 Proof.
 unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
@@ -166,7 +166,7 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd.
+Instance NZmul_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmul.
 Proof.
 unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
@@ -189,17 +189,13 @@ Qed.
 Section Induction.
 Open Scope NatScope. (* automatically closes at the end of the section *)
 Variable A : Z -> Prop.
-Hypothesis A_wd : predicate_wd Zeq A.
-
-Add Morphism A with signature Zeq ==> iff as A_morph.
-Proof.
-exact A_wd.
-Qed.
+Hypothesis A_wd : Proper (Zeq==>iff) A.
 
 Theorem NZinduction :
-  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
+  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
+  (* 0 is interpreted as in Z due to "Bind" directive *)
 Proof.
-intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
+intros A0 AS n; unfold NZ0, Zsucc, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
@@ -266,7 +262,7 @@ Definition NZle := Zle.
 Definition NZmin := Zmin.
 Definition NZmax := Zmax.
 
-Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
+Instance NZlt_wd : Proper (Zeq ==> Zeq ==> iff) NZlt.
 Proof.
 unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
 stepr (snd m1 + fst m2) by apply add_comm.
@@ -285,7 +281,7 @@ now stepl (fst m1 + snd m2) by apply add_comm.
 stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm.
 Qed.
 
-Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
+Instance NZle_wd : Proper (Zeq ==> Zeq ==> iff) NZle.
 Proof.
 unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 do 2 rewrite lt_eq_cases. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int.
@@ -293,7 +289,7 @@ fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%I
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
+Instance NZmin_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmin.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
@@ -309,7 +305,7 @@ stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
 unfold Zeq in H2. rewrite H2. ring.
 Qed.
 
-Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
+Instance NZmax_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmax.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
@@ -372,7 +368,7 @@ Definition Zopp (n : Z) : Z := (snd n, fst n).
 
 Notation "- x" := (Zopp x) : IntScope.
 
-Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
+Instance Zopp_wd : Proper (Zeq ==> Zeq) Zopp.
 Proof.
 unfold Zeq; intros n m H; simpl. symmetry.
 stepl (fst n + snd m) by apply add_comm.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3e029d81b..823ef149c 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -32,6 +32,7 @@ Hint Rewrite
  Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec.
 
 Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec.
+Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
@@ -47,30 +48,13 @@ Definition NZmul := Z.mul.
 
 Instance NZeq_equiv : Equivalence Z.eq.
 
-Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
+Obligation Tactic := zcongruence.
 
-Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
-
-Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
-
-Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
-
-Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
+Program Instance NZsucc_wd : Proper (Z.eq ==> Z.eq) NZsucc.
+Program Instance NZpred_wd : Proper (Z.eq ==> Z.eq) NZpred.
+Program Instance NZadd_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZadd.
+Program Instance NZsub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZsub.
+Program Instance NZmul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZmul.
 
 Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n.
 Proof.
@@ -80,13 +64,10 @@ Qed.
 Section Induction.
 
 Variable A : Z.t -> Prop.
-Hypothesis A_wd : predicate_wd Z.eq A.
+Hypothesis A_wd : Proper (Z.eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (Z.succ n).
 
-Add Morphism A with signature Z.eq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
-
 Let B (z : Z) := A (Z.of_Z z).
 
 Lemma B0 : B 0.
@@ -204,30 +185,30 @@ Proof.
  rewrite spec_compare_alt; destruct Zcompare; auto.
 Qed.
 
-Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
+Instance compare_wd : Proper (Z.eq ==> Z.eq ==> eq) Z.compare.
 Proof.
 intros x x' Hx y y' Hy.
 rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
+Instance NZlt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.
 Proof.
 intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd.
+Instance NZle_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.le.
 Proof.
 intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd.
+Instance NZmin_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.min.
 Proof.
-intros; red; rewrite 2 spec_min; congruence.
+repeat red; intros; rewrite 2 spec_min; congruence.
 Qed.
 
-Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd.
+Instance NZmax_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.max.
 Proof.
-intros; red; rewrite 2 spec_max; congruence.
+repeat red; intros; rewrite 2 spec_max; congruence.
 Qed.
 
 Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
@@ -274,10 +255,7 @@ End NZOrdAxiomsMod.
 
 Definition Zopp := Z.opp.
 
-Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd.
-Proof.
-intros; zsimpl; auto with zarith.
-Qed.
+Program Instance Zopp_wd : Proper (Z.eq ==> Z.eq) Z.opp.
 
 Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n.
 Proof.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 7ad38577f..0c9d006d6 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -56,10 +56,7 @@ Section CentralInduction.
 
 Variable A : predicate NZ.
 
-Hypothesis A_wd : predicate_wd NZeq A.
-
-Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
+Hypothesis A_wd : Proper (NZeq==>iff) A.
 
 Theorem NZcentral_induction :
   forall z : NZ, A z ->
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index e8c292992..85b284a72 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -394,10 +394,7 @@ in the induction step *)
 Section Induction.
 
 Variable A : NZ -> Prop.
-Hypothesis A_wd : predicate_wd NZeq A.
-
-Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
+Hypothesis A_wd : Proper (NZeq==>iff) A.
 
 Section Center.
 
@@ -557,8 +554,7 @@ Theorem NZorder_induction' :
 Proof.
 intros Az AS AP n; apply NZorder_induction; try assumption.
 intros m H1 H2. apply AP in H2; [| now apply <- NZle_succ_l].
-unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
-[assumption | apply NZpred_succ].
+apply -> (A_wd (P (S m)) m); [assumption | apply NZpred_succ].
 Qed.
 
 End Center.
@@ -615,26 +611,24 @@ Variable z : NZ.
 Let Rlt (n m : NZ) := z <= n /\ n < m.
 Let Rgt (n m : NZ) := m < n /\ n <= z.
 
-Add Morphism Rlt with signature NZeq ==> NZeq ==> iff as Rlt_wd.
+Instance Rlt_wd : Proper (NZeq ==> NZeq ==> iff) Rlt.
 Proof.
-intros x1 x2 H1 x3 x4 H2; unfold Rlt; rewrite H1; now rewrite H2.
+intros x1 x2 H1 x3 x4 H2; unfold Rlt. rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism Rgt with signature NZeq ==> NZeq ==> iff as Rgt_wd.
+Instance Rgt_wd : Proper (NZeq ==> NZeq ==> iff) Rgt.
 Proof.
 intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
 Qed.
 
-Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc Rlt).
+Instance NZAcc_lt_wd : Proper (NZeq==>iff) (Acc Rlt).
 Proof.
-unfold predicate_wd, fun_wd.
 intros x1 x2 H; split; intro H1; destruct H1 as [H2];
 constructor; intros; apply H2; now (rewrite H || rewrite <- H).
 Qed.
 
-Lemma NZAcc_gt_wd : predicate_wd NZeq (Acc Rgt).
+Instance NZAcc_gt_wd : Proper (NZeq==>iff) (Acc Rgt).
 Proof.
-unfold predicate_wd, fun_wd.
 intros x1 x2 H; split; intro H1; destruct H1 as [H2];
 constructor; intros; apply H2; now (rewrite H || rewrite <- H).
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 60b43f0d2..02d82bacd 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -129,7 +129,7 @@ symmetry in H; false_hyp H neq_succ_0.
 Qed.
 
 Theorem induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
 Proof.
 intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption.
@@ -146,7 +146,7 @@ from NZ. *)
 Ltac induct n := induction_maker n ltac:(apply induction).
 
 Theorem case_analysis :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
 Proof.
 intros; apply induction; auto.
@@ -206,12 +206,7 @@ Fibonacci numbers *)
 Section PairInduction.
 
 Variable A : N -> Prop.
-Hypothesis A_wd : predicate_wd Neq A.
-
-Add Morphism A with signature Neq ==> iff as A_morph.
-Proof.
-exact A_wd.
-Qed.
+Hypothesis A_wd : Proper (Neq==>iff) A.
 
 Theorem pair_induction :
   A 0 -> A 1 ->
@@ -230,12 +225,7 @@ End PairInduction.
 Section TwoDimensionalInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : relation_wd Neq Neq R.
-
-Add Morphism R with signature Neq ==> Neq ==> iff as R_morph.
-Proof.
-exact R_wd.
-Qed.
+Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
 
 Theorem two_dim_induction :
    R 0 0 ->
@@ -260,12 +250,7 @@ End TwoDimensionalInduction.
 Section DoubleInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : relation_wd Neq Neq R.
-
-Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1.
-Proof.
-exact R_wd.
-Qed.
+Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
 
 Theorem double_induction :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index e2a6df1cc..1e1cd95c7 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -24,7 +24,7 @@ Definition def_add (x y : N) := recursion y (fun _ p => S p) x.
 
 Infix Local "++" := def_add (at level 50, left associativity).
 
-Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd.
+Instance def_add_wd : Proper (Neq ==> Neq ==> Neq) as def_add.
 Proof.
 unfold def_add.
 intros x x' Exx' y y' Eyy'.
@@ -72,7 +72,7 @@ Proof.
 unfold fun2_eq; intros; apply def_add_wd; assumption.
 Qed.
 
-Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd.
+Instance def_mul_wd : Proper (Neq ==> Neq ==> Neq) def_mul.
 Proof.
 unfold def_mul.
 intros x x' Exx' y y' Eyy'.
@@ -136,7 +136,7 @@ apply lt_step_wd.
 assumption.
 Qed.
 
-Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd.
+Instance def_ltb_wd : Proper (Neq ==> Neq ==> eq) def_ltb.
 Proof.
 intros; now apply lt_curry_wd.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index da48d2fe0..6ecf7fd33 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -32,13 +32,13 @@ Definition homomorphism (f : N1 -> N2) : Prop :=
 Definition natural_isomorphism : N1 -> N2 :=
   NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p).
 
-Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd.
+Instance natural_isomorphism_wd : Proper (Eq1 ==> Eq2) natural_isomorphism.
 Proof.
 unfold natural_isomorphism.
 intros n m Eqxy.
 apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
 reflexivity.
-unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
+intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
 assumption.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index aee2cf8f7..a5b496ba3 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -201,21 +201,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem right_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
         forall n : N, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem left_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, n < z -> A (S n) -> A n) ->
         forall n : N, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem right_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
       (forall n : N, n <= z -> A n) ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
@@ -223,7 +223,7 @@ Theorem right_induction' :
 Proof NZright_induction'.
 
 Theorem left_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
     (forall n : N, z <= n -> A n) ->
     (forall n : N, n < z -> A (S n) -> A n) ->
@@ -231,21 +231,21 @@ Theorem left_induction' :
 Proof NZleft_induction'.
 
 Theorem strong_right_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
     (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
        forall n : N, z <= n -> A n.
 Proof NZstrong_right_induction.
 
 Theorem strong_left_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
       (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
         forall n : N, n <= z -> A n.
 Proof NZstrong_left_induction.
 
 Theorem strong_right_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
       (forall n : N, n <= z -> A n) ->
       (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
@@ -253,7 +253,7 @@ Theorem strong_right_induction' :
 Proof NZstrong_right_induction'.
 
 Theorem strong_left_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
     (forall n : N, z <= n -> A n) ->
     (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
@@ -261,7 +261,7 @@ Theorem strong_left_induction' :
 Proof NZstrong_left_induction'.
 
 Theorem order_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
       (forall n : N, n < z  -> A (S n) -> A n) ->
@@ -269,7 +269,7 @@ Theorem order_induction :
 Proof NZorder_induction.
 
 Theorem order_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
       (forall n : N, n <= z -> A n -> A (P n)) ->
@@ -282,7 +282,7 @@ ZOrder) since they boil down to regular induction *)
 (** Elimintation principle for < *)
 
 Theorem lt_ind :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall n : N,
       A (S n) ->
       (forall m : N, n < m -> A m -> A (S m)) ->
@@ -292,7 +292,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem le_ind :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall n : N,
       A n ->
       (forall m : N, n <= m -> A m -> A (S m)) ->
@@ -309,8 +309,7 @@ Proof NZgt_wf.
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-setoid_replace lt with (fun n m : N => 0 <= n /\ n < m)
-  using relation (@relations_eq N N).
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m).
 apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
@@ -400,13 +399,8 @@ Qed.
 
 Section RelElim.
 
-(* FIXME: Variable R : relation N. -- does not work *)
-
-Variable R : N -> N -> Prop.
-Hypothesis R_wd : relation_wd Neq Neq R.
-
-Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
-Proof. apply R_wd. Qed.
+Variable R : relation N.
+Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
 
 Theorem le_ind_rel :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index a9eec350f..dea4d664d 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -26,13 +26,7 @@ Variable Aeq : relation A.
 
 Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity).
 
-Hypothesis Aeq_equiv : equiv A Aeq.
-
-Add Relation A Aeq
- reflexivity proved by (proj1 Aeq_equiv)
- symmetry proved by (proj2 (proj2 Aeq_equiv))
- transitivity proved by (proj1 (proj2 Aeq_equiv))
-as Aeq_rel.
+Instance Aeq_equiv : Equivalence Aeq.
 
 Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A :=
 recursion
@@ -42,10 +36,7 @@ recursion
   n.
 
 Theorem strong_rec_wd :
-forall a a' : A, a ==A a' ->
-  forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' ->
-    forall n n', n == n' ->
-      strong_rec a f n ==A strong_rec a' f' n'.
+ Proper (Aeq ==> (Neq ==> (Neq ==>Aeq) ==> Aeq) ==> Neq ==> Aeq) strong_rec.
 Proof.
 intros a a' Eaa' f f' Eff' n n' Enn'.
 (* First we prove that recursion (which is on type N -> A) returns
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index c5122ac08..5242826c6 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -32,34 +32,14 @@ Definition NZsub := Nminus.
 Definition NZmul := Nmult.
 
 Instance NZeq_equiv : Equivalence NZeq.
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc.
+Program Instance NZpred_wd : Proper (eq==>eq) NZpred.
+Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd.
+Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub.
+Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul.
 
 Theorem NZinduction :
-  forall A : NZ -> Prop, predicate_wd NZeq A ->
+  forall A : NZ -> Prop, Proper (NZeq==>iff) A ->
     A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n.
 Proof.
 intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS.
@@ -117,25 +97,10 @@ Definition NZle := Nle.
 Definition NZmin := Nmin.
 Definition NZmax := Nmax.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt.
+Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle.
+Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin.
+Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax.
 
 Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m.
 Proof.
@@ -199,14 +164,9 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem recursion_wd :
-forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
-      forall x x' : N, x = x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd A (Aeq : relation A) :
+ Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A).
 Proof.
-unfold fun2_wd, NZeq, fun2_eq.
 intros A Aeq a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nrect.
 intros x' H; now rewrite <- H.
@@ -224,10 +184,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
-    Aeq a a -> fun2_wd NZeq Aeq Aeq f ->
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)).
 Proof.
-unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect.
+unfold recursion; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect.
 rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.
 clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
 now rewrite Nrect_step.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 38951218d..61171a43e 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -29,38 +29,14 @@ Definition NZsub := minus.
 Definition NZmul := mult.
 
 Instance NZeq_equiv : Equivalence NZeq.
-
-(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq"
-then the theorem generated for succ_wd below is forall x, succ x = succ x,
-which does not match the axioms in NAxiomsSig *)
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc.
+Program Instance NZpred_wd : Proper (eq==>eq) NZpred.
+Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd.
+Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub.
+Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul.
 
 Theorem NZinduction :
-  forall A : nat -> Prop, predicate_wd (@eq nat) A ->
+  forall A : nat -> Prop, Proper (eq==>iff) A ->
     A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
 Proof.
 intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
@@ -108,25 +84,10 @@ Definition NZle := le.
 Definition NZmin := min.
 Definition NZmax := max.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt.
+Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle.
+Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin.
+Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax.
 
 Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.
 Proof.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 596603b6f..81893d9af 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -41,26 +41,26 @@ Definition NZmul := N.mul.
 
 Instance NZeq_equiv : Equivalence N.eq.
 
-Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
+Instance NZsucc_wd : Proper (N.eq==>N.eq) NZsucc.
 Proof.
-unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto.
+unfold N.eq; repeat red; intros; rewrite 2 N.spec_succ; f_equal; auto.
 Qed.
 
-Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd.
+Instance NZpred_wd : Proper (N.eq==>N.eq) NZpred.
 Proof.
-unfold N.eq; intros.
+unfold N.eq; repeat red; intros.
 generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0).
 destruct N.eq_bool; rewrite N.spec_0; intros.
 rewrite 2 N.spec_pred0; congruence.
 rewrite 2 N.spec_pred; f_equal; auto; try omega.
 Qed.
 
-Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd.
+Instance NZadd_wd : Proper (N.eq==>N.eq==>N.eq) NZadd.
 Proof.
-unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
+unfold N.eq; repeat red; intros; rewrite 2 N.spec_add; f_equal; auto.
 Qed.
 
-Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd.
+Instance NZsub_wd : Proper (N.eq==>N.eq==>N.eq) NZsub.
 Proof.
 unfold N.eq; intros x x' Hx y y' Hy.
 destruct (Z_lt_le_dec [x] [y]).
@@ -68,14 +68,14 @@ rewrite 2 N.spec_sub0; f_equal; congruence.
 rewrite 2 N.spec_sub; f_equal; congruence.
 Qed.
 
-Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd.
+Instance NZmul_wd : Proper (N.eq==>N.eq==>N.eq) NZmul.
 Proof.
-unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto.
+unfold N.eq; repeat red; intros; rewrite 2 N.spec_mul; f_equal; auto.
 Qed.
 
 Theorem NZpred_succ : forall n, N.pred (N.succ n) == n.
 Proof.
-unfold N.eq; intros.
+unfold N.eq; repeat red; intros.
 rewrite N.spec_pred; rewrite N.spec_succ.
 omega.
 generalize (N.spec_pos n); omega.
@@ -86,13 +86,10 @@ Definition N_of_Z z := N.of_N (Zabs_N z).
 Section Induction.
 
 Variable A : N.t -> Prop.
-Hypothesis A_wd : predicate_wd N.eq A.
+Hypothesis A_wd : Proper (N.eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (N.succ n).
 
-Add Morphism A with signature N.eq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
-
 Let B (z : Z) := A (N_of_Z z).
 
 Lemma B0 : B 0.
@@ -211,30 +208,30 @@ Proof.
  rewrite spec_compare_alt; destruct Zcompare; auto.
 Qed.
 
-Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
+Instance compare_wd : Proper (N.eq ==> N.eq ==> eq) N.compare.
 Proof.
 intros x x' Hx y y' Hy.
 rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.
+Instance NZlt_wd : Proper (N.eq ==> N.eq ==> iff) N.lt.
 Proof.
 intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd.
+Instance NZle_wd : Proper (N.eq ==> N.eq ==> iff) N.le.
 Proof.
 intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd.
+Instance NZmin_wd : Proper (N.eq ==> N.eq ==> N.eq) N.min.
 Proof.
-intros; red; rewrite 2 spec_min; congruence.
+repeat red; intros; rewrite 2 spec_min; congruence.
 Qed.
 
-Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd.
+Instance NZmax_wd : Proper (N.eq ==> N.eq ==> N.eq) N.max.
 Proof.
-intros; red; rewrite 2 spec_max; congruence.
+repeat red; intros; rewrite 2 spec_max; congruence.
 Qed.
 
 Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
@@ -313,10 +310,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
-    Aeq a a -> fun2_wd N.eq Aeq Aeq f ->
+    Aeq a a -> Proper (N.eq==>Aeq==>Aeq) f ->
       forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)).
 Proof.
-unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n.
+unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n.
 replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)).
 rewrite Nrect_step.
 apply f_wd; auto.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index ddd1c50c3..290c9b1c2 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -91,75 +91,31 @@ end.
 
 Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r].
 
-(** Extentional properties of predicates, relations and functions *)
+(** Predicates, relations, functions *)
 
 Definition predicate (A : Type) := A -> Prop.
 
-Section ExtensionalProperties.
-
-Variables A B C : Type.
-Variable Aeq : relation A.
-Variable Beq : relation B.
-Variable Ceq : relation C.
-
-(* "wd" stands for "well-defined" *)
-
-Definition fun_wd (f : A -> B) := Proper (Aeq==>Beq) f.
-
-Definition fun2_wd (f : A -> B -> C) := Proper (Aeq==>Beq==>Ceq) f.
-
-Definition fun_eq : relation (A -> B) := (Aeq==>Beq)%signature.
-
-(* Note that reflexivity of fun_eq means that every function
-is well-defined w.r.t. Aeq and Beq, i.e.,
-forall x x' : A, Aeq x x' -> Beq (f x) (f x') *)
-
-Definition fun2_eq (f f' : A -> B -> C) := (Aeq==>Beq==>Ceq)%signature f f'.
-
-End ExtensionalProperties.
-
-(* The following definitions instantiate Beq or Ceq to iff; therefore, they
-have to be outside the ExtensionalProperties section *)
-
-Definition predicate_wd (A : Type) (Aeq : relation A) := Proper (Aeq==>iff).
-
-Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
-  Proper (Aeq==>Beq==>iff).
-
-Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) :=
-  forall (x : A) (y : B), R1 x y <-> R2 x y.
-
-Instance relation_eq_equiv A B : Equivalence (@relations_eq A B).
-Proof.
-intros A B; split;
-unfold Reflexive, Symmetric, Transitive, relations_eq.
-reflexivity.
-now symmetry.
-intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
-Qed.
-
-Instance well_founded_wd A : Proper (@relations_eq A A ==> iff) (@well_founded A).
+Instance well_founded_wd A :
+ Proper (@relation_equivalence A ==> iff) (@well_founded A).
 Proof.
-unfold relations_eq, well_founded; intros A R1 R2 H.
-split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
-intros y H4; apply H3; [now apply <- H | now apply -> H].
+intros A R1 R2 H.
+split; intros WF a; induction (WF a) as [x _ WF']; constructor;
+intros y Ryx; apply WF'; destruct (H y x); auto.
 Qed.
 
-(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of
-morhisms and quatifiers *)
+(** [solve_predicate_wd] solves the goal [Proper (?==>iff) P]
+    for P consisting of morphisms and quantifiers *)
 
 Ltac solve_predicate_wd :=
-unfold predicate_wd;
 let x := fresh "x" in
 let y := fresh "y" in
 let H := fresh "H" in
   intros x y H; setoid_rewrite H; reflexivity.
 
-(* solve_relation_wd solves the goal [relation_wd R] for R consisting of
-morhisms and quatifiers *)
+(** [solve_relation_wd] solves the goal [Proper (?==>?==>iff) R]
+    for R consisting of morphisms and quantifiers *)
 
 Ltac solve_relation_wd :=
-unfold relation_wd, fun2_wd;
 let x1 := fresh "x" in
 let y1 := fresh "y" in
 let H1 := fresh "H" in
@@ -181,39 +137,3 @@ Ltac induction_maker n t :=
   pattern n; t; clear n;
   [solve_predicate_wd | ..].
 
-(** Relations on cartesian product. Used in MiscFunct for defining
-functions whose domain is a product of sets by primitive recursion *)
-
-Section RelationOnProduct.
-
-Variables A B : Set.
-Variable Aeq : relation A.
-Variable Beq : relation B.
-
-Definition prod_rel : relation (A * B) := (Aeq * Beq)%signature.
-
-Instance prod_rel_equiv `(Equivalence _ Aeq, Equivalence _ Beq) :
- Equivalence prod_rel.
-
-End RelationOnProduct.
-
-Implicit Arguments prod_rel [A B].
-Implicit Arguments prod_rel_equiv [A B].
-
-(** Miscellaneous *)
-
-(*Definition comp_bool (x y : comparison) : bool :=
-match x, y with
-| Lt, Lt => true
-| Eq, Eq => true
-| Gt, Gt => true
-| _, _   => false
-end.
-
-Theorem comp_bool_correct : forall x y : comparison,
-  comp_bool x y <-> x = y.
-Proof.
-destruct x; destruct y; simpl; split; now intro.
-Qed.*)
-
-
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 4177fc202..38542c12b 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -62,40 +62,42 @@ Open Scope bigQ_scope.
 
 (** [BigQ] is a setoid *)
 
-Add Relation BigQ.t BigQ.eq
- reflexivity proved by (fun x => Qeq_refl [x])
- symmetry proved by (fun x y => Qeq_sym [x] [y])
- transitivity proved by (fun x y z => Qeq_trans [x] [y] [z])
-as BigQeq_rel.
+Instance BigQeq_rel : Equivalence BigQ.eq.
 
-Add Morphism BigQ.add with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQadd_wd.
+Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add.
 Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_add; rewrite H, H0; apply Qeq_refl.
+ do 3 red. unfold BigQ.eq; intros.
+ rewrite !BigQ.spec_add, H, H0. reflexivity.
 Qed.
 
-Add Morphism BigQ.opp with signature BigQ.eq ==> BigQ.eq as BigQopp_wd.
+Instance BigQopp_wd : Proper (BigQ.eq==>BigQ.eq) BigQ.opp.
 Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_opp; rewrite H; apply Qeq_refl.
+ do 2 red. unfold BigQ.eq; intros.
+ rewrite !BigQ.spec_opp, H; reflexivity.
 Qed.
 
-Add Morphism BigQ.sub with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQsub_wd.
+Instance BigQsub_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.sub.
 Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_sub; rewrite H, H0; apply Qeq_refl.
+ do 3 red. unfold BigQ.eq; intros.
+ rewrite !BigQ.spec_sub, H, H0; reflexivity.
 Qed.
 
-Add Morphism BigQ.mul with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQmul_wd.
+Instance BigQmul_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.mul.
 Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_mul; rewrite H, H0; apply Qeq_refl.
+ do 3 red. unfold BigQ.eq; intros.
+ rewrite !BigQ.spec_mul, H, H0; reflexivity.
 Qed.
 
-Add Morphism BigQ.inv with signature BigQ.eq ==> BigQ.eq as BigQinv_wd.
+Instance BigQinv_wd : Proper (BigQ.eq==>BigQ.eq) BigQ.inv.
 Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_inv; rewrite H; apply Qeq_refl.
+ do 2 red; unfold BigQ.eq; intros.
+ rewrite !BigQ.spec_inv, H; reflexivity.
 Qed.
 
-Add Morphism BigQ.div with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQdiv_wd.
+Instance BigQdiv_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.div.
 Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_div; rewrite H, H0; apply Qeq_refl.
+ do 3 red; unfold BigQ.eq; intros.
+ rewrite !BigQ.spec_div, H, H0; reflexivity.
 Qed.
 
 (* TODO : fix this. For the moment it's useless (horribly slow)