Adaptation des fichiers de micromega suite aux changements dans

setoid_rewrite, et dans Romega.

Pour info, ces fichiers ne sont pas compilés... (?)



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

1 files changed, 11 insertions, 7 deletions

diff --git a/contrib/micromega/RingMicromega.v b/contrib/micromega/RingMicromega.v
index b118f8d99..5aca6e697 100644
--- a/contrib/micromega/RingMicromega.v
+++ b/contrib/micromega/RingMicromega.v
@@ -71,9 +71,9 @@ Record SORaddon := mk_SOR_addon {
 Variable addon : SORaddon.
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
-  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
-  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
 as micomega_sor_setoid.
 
 Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
@@ -90,15 +90,17 @@ exact sor.(SORopp_wd).
 Qed.
 Add Morphism rle with signature req ==> req ==> iff as rle_morph.
 Proof.
-exact sor.(SORle_wd).
+  exact sor.(SORle_wd).
 Qed.
 Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
 Proof.
-exact sor.(SORlt_wd).
+  exact sor.(SORlt_wd).
 Qed.
 
 Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
-Proof (rminus_morph sor). (* We already proved that minus is a morphism in OrderedRing.v *)
+Proof.
+  exact (rminus_morph sor). (* We already proved that minus is a morphism in OrderedRing.v *)
+Qed.
 
 Definition cneqb (x y : C) := negb (ceqb x y).
 Definition cltb (x y : C) := (cleb x y) && (cneqb x y).
@@ -111,7 +113,9 @@ Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption
 Ltac le_elim H := rewrite (Rle_lt_eq sor) in H; destruct H as [H | H].
 
 Lemma cleb_sound : forall x y : C, x [<=] y = true -> [x] <= [y].
-Proof addon.(SORcleb_morph).
+Proof.
+  exact addon.(SORcleb_morph).
+Qed.
 
 Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
 Proof.