Plug the new setoid implemtation in, leaving the original one commented

out. The semantics of the old setoid are faithfully simulated by the new
tactic, hence no scripts involving rewrite are modified. However,
parametric morphism declarations need to be changed, but there are only a
few in the standard library, notably in FSets. The declaration and the
introduction of variables in the script need to be tweaked a bit,
otherwise the proofs remain unchanged. 
Some fragile scripts not introducting their variable names explicitely
were broken. Requiring Setoid requires Program.Basics which sets stronger
implicit arguments on some constants, a few scripts benefit from that.
Ring/field have been ported but do not really use the new typeclass
architecture as well as they could. Performance should be mostly
unchanged, but will certainly improve in the near future. Size of the
vo's seems not to have changed at all.
It will certainly break some contribs using Setoid.


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

6 files changed, 11 insertions, 11 deletions

diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index db09c2ec7..e885d25bc 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -143,7 +143,7 @@ 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 A_wd.
+Proof. apply A_wd. Qed.
 
 Let B (n : Z) := A (Z_to_NZ n).
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 730d8a00f..084560de3 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -64,7 +64,7 @@ something like this. The same goes for "relation". *)
 Hypothesis A_wd : predicate_wd NZeq A.
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Theorem NZcentral_induction :
   forall z : NZ, A z ->
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 0708e060a..bc3600f9c 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -396,7 +396,7 @@ Variable A : NZ -> Prop.
 Hypothesis A_wd : predicate_wd NZeq A.
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Section Center.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0a3d1a586..27d9c72bd 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd.
+Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 9ddaa9a2f..7b4645be3 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -407,7 +407,7 @@ 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 R_wd.
+Proof. apply R_wd. Qed.
 
 Theorem le_ind_rel :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index e66bc8ebf..c063c7bc1 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -148,15 +148,15 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 now symmetry.
 Qed.
 
-Add Relation (fun A B : Type => A -> B -> Prop) relations_eq
-  reflexivity proved by (fun A B : Type => proj1 (relations_eq_equiv A B))
-  symmetry proved by (fun A B : Type => proj2 (proj2 (relations_eq_equiv A B)))
-  transitivity proved by (fun A B : Type => proj1 (proj2 (relations_eq_equiv A B)))
+Add Relation (A -> B -> Prop) (@relations_eq A B)
+  reflexivity proved by (proj1 (relations_eq_equiv A B))
+  symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
+  transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
 as relations_eq_rel.
 
-Add Morphism well_founded with signature relations_eq ==> iff as well_founded_wd.
+Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
 Proof.
-unfold relations_eq, well_founded; intros A R1 R2 H;
+unfold relations_eq, well_founded; intros 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].
 Qed.