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

1 files changed, 2 insertions, 2 deletions

diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v
index 67a952b73..d410606a7 100644
--- a/contrib/rtauto/Bintree.v
+++ b/contrib/rtauto/Bintree.v
@@ -107,7 +107,7 @@ intro ne;right;congruence.
 left;reflexivity.
 Defined.
 
-Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (m<>m) (refl_equal m) .
+Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m).
 fix 1;intros [mm|mm|].
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
@@ -116,7 +116,7 @@ Qed.
 
 Theorem pos_eq_dec_ex : forall m n,
  pos_eq m n =true -> exists h:m=n,
- pos_eq_dec m n = left (m<>n) h.
+ pos_eq_dec m n = left h.
 fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
 simpl;intro e.
 elim (pos_eq_dec_ex _ _ e).