Modularization of BinPos + fixes in Stdlib

 BinPos now contain a sub-module Pos, in which are placed functions
 like add (ex-Pplus), mul (ex-Pmult), ... and properties like
 add_comm, add_assoc, ...

 In addition to the name changes, the organisation is changed quite
 a lot, to try to take advantage more of the orders < and <= instead
 of speaking only of the comparison function.

 The main source of incompatibilities in scripts concerns this compare:
 Pos.compare is now a binary operation, expressed in terms of the
 ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
 this ternary version being called now Pos.compare_cont. As for everything
 else, compatibility notations (only parsing) are provided. But notations
 "_ ?= _" on positive will have to be edited, since they now point to
 Pos.compare.

 We also make the sub-module Pos to be directly an OrderedType,
 and include results about min and max.

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

2 files changed, 13 insertions, 13 deletions

diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index f72933f99..309ebdef1 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -105,12 +105,12 @@ Section MakeRingPol.
   match P, P' with
   | Pc c, Pc c' => c ?=! c'
   | Pinj j Q, Pinj j' Q' =>
-    match Pcompare j j' Eq with
+    match j ?= j' with
     | Eq => Peq Q Q'
     | _ => false
     end
   | PX P i Q, PX P' i' Q' =>
-    match Pcompare i i' Eq with
+    match i ?= i' with
     | Eq => if Peq P P' then Peq Q Q' else false
     | _ => false
     end
@@ -421,7 +421,7 @@ Section MakeRingPol.
         _, mon0 => (Pc cO, P)
    | Pc _, _    => (P, Pc cO)
    | Pinj j1 P1, zmon j2 M1 =>
-      match (j1 ?= j2) Eq with
+      match (j1 ?= j2) with
         Eq => let (R,S) := MFactor P1 M1 in
                  (mkPinj j1 R, mkPinj j1 S)
       | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in
@@ -435,7 +435,7 @@ Section MakeRingPol.
              let (R2, S2) := MFactor Q1 M2 in
                (mkPX R1 i R2, mkPX S1 i S2)
   | PX P1 i Q1, vmon j M1 =>
-      match (i ?= j) Eq with
+      match (i ?= j) with
         Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
                  (mkPX R1 i Q1, S1)
       | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in
@@ -537,10 +537,10 @@ Section MakeRingPol.
  Proof.
   induction P;destruct P';simpl;intros;try discriminate;trivial.
   apply (morph_eq CRmorph);trivial.
-  assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
+  assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
    try discriminate H.
   rewrite (IHP P' H); rewrite H1;trivial;rrefl.
-  assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
+  assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
    try discriminate H.
   rewrite H1;trivial. clear H1.
   assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2);
@@ -1019,8 +1019,8 @@ Qed.
    intros i P Hrec M l; case M; simpl; clear M.
      rewrite (morph0 CRmorph); rsimpl.
      intros j M.
-     case_eq ((i ?= j) Eq); intros He; simpl.
-       rewrite (Pcompare_Eq_eq _ _ He).
+     case_eq (i ?= j); intros He; simpl.
+       rewrite (Pos.compare_eq _ _ He).
        generalize (Hrec M (jump j l)); case (MFactor P M);
         simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
        generalize (Hrec (zmon (j -i) M) (jump i l));
@@ -1048,8 +1048,8 @@ Qed.
      rewrite (ARadd_comm ARth); rsimpl.
      rewrite zmon_pred_ok;rsimpl.
    intros j M1.
-     case_eq ((i ?= j) Eq); intros He; simpl.
-       rewrite (Pcompare_Eq_eq _ _ He).
+     case_eq (i ?= j); intros He; simpl.
+       rewrite (Pos.compare_eq _ _ He).
        generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1));
         simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
        rewrite H; rewrite mkPX_ok; rsimpl.
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index f8df97489..2bf3d8c35 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -138,7 +138,7 @@ Qed.
 
 Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
 Proof.
-unfold Zlt; intros x y H;
+intros x y H.
 do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt));
 destruct x; destruct y; simpl in *; try discriminate.
 apply phi_pos1_pos.
@@ -146,8 +146,8 @@ now apply clt_pos_morph.
 apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
 apply (Rlt_trans sor) with 0. apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
 apply phi_pos1_pos.
-rewrite Pcompare_antisym in H; simpl in H. apply -> (Ropp_lt_mono sor).
-now apply clt_pos_morph.
+apply -> (Ropp_lt_mono sor); apply clt_pos_morph.
+red. now rewrite Pos.compare_antisym.
 Qed.
 
 Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y].