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

13 files changed, 167 insertions, 294 deletions

diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 322f43850..fd8ad6d77 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -36,14 +36,16 @@ Extract Inductive N => "Big.big_int"
 
 (** Efficient (but uncertified) versions for usual functions *)
 
-Extract Constant Pplus => "Big.add".
-Extract Constant Psucc => "Big.succ".
-Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)".
-Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)".
-Extract Constant Pmult => "Big.mult".
-Extract Constant Pmin => "Big.min".
-Extract Constant Pmax => "Big.max".
-Extract Constant Pcompare =>
+Extract Constant Pos.add => "Big.add".
+Extract Constant Pos.succ => "Big.succ".
+Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)".
+Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)".
+Extract Constant Pos.mul => "Big.mult".
+Extract Constant Pos.min => "Big.min".
+Extract Constant Pos.max => "Big.max".
+Extract Constant Pos.compare =>
+ "fun x y -> Big.compare_case Eq Lt Gt x y".
+Extract Constant Pos.compare_cont =>
  "fun x y c -> Big.compare_case c Lt Gt x y".
 
 Extract Constant Nplus => "Big.add".
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 9044b9384..013695772 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -33,14 +33,16 @@ Extract Inductive N => int [ "0" "" ]
 
 (** Efficient (but uncertified) versions for usual functions *)
 
-Extract Constant Pplus => "(+)".
-Extract Constant Psucc => "succ".
-Extract Constant Ppred => "fun n -> max 1 (n-1)".
-Extract Constant Pminus => "fun n m -> max 1 (n-m)".
-Extract Constant Pmult => "( * )".
-Extract Constant Pmin => "min".
-Extract Constant Pmax => "max".
-Extract Constant Pcompare =>
+Extract Constant Pos.add => "(+)".
+Extract Constant Pos.succ => "succ".
+Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
+Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
+Extract Constant Pos.mul => "( * )".
+Extract Constant Pos.min => "min".
+Extract Constant Pos.max => "max".
+Extract Constant Pos.compare =>
+ "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
+Extract Constant Pos.compare_cont =>
  "fun x y c -> if x=y then c else if x<y then Lt else Gt".
 
 
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].
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index a5a085a99..f6b00bd86 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -223,17 +223,17 @@ Ltac zify_positive_rel :=
   | H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
   | |- context [ @eq positive ?a ?b ] =>       rewrite (Zpos_eq_iff a b)
   (* II: less than *)
-  | H : context [ (?a<?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
-  | |- context [ (?a<?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
+  | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
+  | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
   (* III: less or equal *)
-  | H : context [ (?a<=?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
-  | |- context [ (?a<=?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
+  | H : context [ (?a <= ?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
+  | |- context [ (?a <= ?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
   (* IV: greater than *)
-  | H : context [ (?a>?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
-  | |- context [ (?a>?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
+  | H : context [ (?a > ?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
+  | |- context [ (?a > ?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
   (* V: greater or equal *)
-  | H : context [ (?a>=?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
-  | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
+  | H : context [ (?a >= ?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
+  | |- context [ (?a >= ?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
  end.
 
 Ltac zify_positive_op :=
@@ -358,25 +358,25 @@ Ltac zify_N_rel :=
   | H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
   | |- context [ @eq N ?a ?b ] =>       rewrite (Z_of_N_eq_iff a b)
   (* II: less than *)
-  | H : (?a<?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
-  | |- (?a<?b)%N => apply (Z_of_N_lt_rev a b)
-  | H : context [ (?a<?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
-  | |- context [ (?a<?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
+  | H : (?a < ?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
+  | |- (?a < ?b)%N => apply (Z_of_N_lt_rev a b)
+  | H : context [ (?a < ?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
+  | |- context [ (?a < ?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
   (* III: less or equal *)
-  | H : (?a<=?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
-  | |- (?a<=?b)%N => apply (Z_of_N_le_rev a b)
-  | H : context [ (?a<=?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
-  | |- context [ (?a<=?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
+  | H : (?a <= ?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
+  | |- (?a <= ?b)%N => apply (Z_of_N_le_rev a b)
+  | H : context [ (?a <= ?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
+  | |- context [ (?a <= ?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
   (* IV: greater than *)
-  | H : (?a>?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
-  | |- (?a>?b)%N => apply (Z_of_N_gt_rev a b)
-  | H : context [ (?a>?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
-  | |- context [ (?a>?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
+  | H : (?a > ?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
+  | |- (?a > ?b)%N => apply (Z_of_N_gt_rev a b)
+  | H : context [ (?a > ?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
+  | |- context [ (?a > ?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
   (* V: greater or equal *)
-  | H : (?a>=?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
-  | |- (?a>=?b)%N => apply (Z_of_N_ge_rev a b)
-  | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
-  | |- context [ (?a>=?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
+  | H : (?a >= ?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
+  | |- (?a >= ?b)%N => apply (Z_of_N_ge_rev a b)
+  | H : context [ (?a >= ?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
+  | |- context [ (?a >= ?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
  end.
 
 Ltac zify_N_op :=
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 6c250ef4f..e3e9078e3 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -12,139 +12,20 @@ Require Export BinPos.
 Open Scope positive_scope.
 
 Ltac clean := try (simpl; congruence).
-Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
-
-Functional Scheme Pcompare_ind := Induction for Pcompare Sort Prop.
-
-Lemma Gt_Eq_Gt : forall p q cmp,
-       (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt.
-apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Eq = Gt -> (p ?= q) cmp = Gt));
-simpl;auto;congruence.
-Qed.
-
-Lemma Gt_Lt_Gt : forall p q cmp,
-       (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt.
-apply (Pcompare_ind (fun p q cmp _ => (p ?= q) Lt = Gt -> (p ?= q) cmp = Gt));
-simpl;auto;congruence.
-Qed.
-
-Lemma Gt_Psucc_Eq: forall p q,
-  (p ?= Psucc q) Gt = Gt -> (p ?= q) Eq = Gt.
-intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
-intro;apply Gt_Eq_Gt;auto.
-apply Gt_Lt_Gt.
-Qed.
-
-Lemma Eq_Psucc_Gt: forall p q,
-  (p ?= Psucc q) Eq = Eq -> (p ?= q) Eq = Gt.
-intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
-intro H;elim (Pcompare_not_Eq p (Psucc q));tauto.
-intro H;apply Gt_Eq_Gt;auto.
-intro H;rewrite Pcompare_Eq_eq with p q;auto.
-generalize q;clear q IHq p H;induction q;simpl;auto.
-intro H;elim (Pcompare_not_Eq p q);tauto.
-Qed.
-
-Lemma Gt_Psucc_Gt : forall n p cmp cmp0,
- (n?=p) cmp = Gt -> (Psucc n?=p) cmp0 = Gt.
-induction n;intros [ | p | p];simpl;try congruence.
-intros; apply IHn with cmp;trivial.
-intros; apply IHn with Gt;trivial.
-intros;apply Gt_Lt_Gt;trivial.
-intros [ | | ] _ H.
-apply Gt_Eq_Gt;trivial.
-apply Gt_Lt_Gt;trivial.
-trivial.
-Qed.
 
 Lemma Gt_Psucc: forall p q,
-       (p ?= Psucc q) Eq = Gt -> (p ?= q) Eq = Gt.
-intros p q;generalize p;clear p;induction q;destruct p;simpl;auto;try congruence.
-apply Gt_Psucc_Eq.
-intro;apply Gt_Eq_Gt;apply IHq;auto.
-apply Gt_Eq_Gt.
-apply Gt_Lt_Gt.
+       (p ?= Psucc q) = Gt -> (p ?= q) = Gt.
+Proof.
+intros. rewrite <- Pos.compare_succ_succ.
+now apply Pos.lt_gt, Pos.lt_lt_succ, Pos.gt_lt.
 Qed.
 
 Lemma Psucc_Gt : forall p,
-       (Psucc p ?= p) Eq = Gt.
-induction p;simpl.
-apply Gt_Eq_Gt;auto.
-generalize p;clear p IHp.
-induction p;simpl;auto.
-reflexivity.
-Qed.
-
-Fixpoint pos_eq (m n:positive) {struct m} :bool :=
-match m, n with
-  xI mm, xI nn => pos_eq mm nn
-| xO mm, xO nn => pos_eq mm nn
-| xH, xH => true
-| _, _ => false
-end.
-
-Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
-induction m;simpl;intro n;destruct n;congruence ||
-(intro e;apply f_equal;auto).
-Defined.
-
-Theorem refl_pos_eq : forall m, pos_eq m m = true.
-induction m;simpl;auto.
+       (Psucc p ?= p) = Gt.
+Proof.
+intros. apply Pos.lt_gt, Pos.lt_succ_diag_r.
 Qed.
 
-Definition pos_eq_dec : forall (m n:positive), {m=n}+{m<>n} .
-fix 1;intros [mm|mm|] [nn|nn|];try (right;congruence).
-case (pos_eq_dec mm nn).
-intro e;left;apply (f_equal xI e).
-intro ne;right;congruence.
-case (pos_eq_dec mm nn).
-intro e;left;apply (f_equal xO e).
-intro ne;right;congruence.
-left;reflexivity.
-Defined.
-
-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.
-reflexivity.
-Qed.
-
-Theorem pos_eq_dec_ex : forall m n,
- pos_eq m n =true -> exists h:m=n,
- 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).
-intros x ex; rewrite ex.
-exists (f_equal xI x).
-reflexivity.
-simpl;intro e.
-elim (pos_eq_dec_ex _ _ e).
-intros x ex; rewrite ex.
-exists (f_equal xO x).
-reflexivity.
-simpl.
-exists (refl_equal xH).
-reflexivity.
-Qed.
-
-Fixpoint nat_eq (m n:nat) {struct m}: bool:=
-match m, n with
-O,O => true
-| S mm,S nn => nat_eq mm nn
-| _,_ => false
-end.
-
-Theorem nat_eq_refl : forall m n, nat_eq m n = true -> m = n.
-induction m;simpl;intro n;destruct n;congruence ||
-(intro e;apply f_equal;auto).
-Defined.
-
-Theorem refl_nat_eq : forall n, nat_eq n n = true.
-induction n;simpl;trivial.
-Defined.
-
 Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A :=
 match l with nil => None
 | x::q =>
@@ -178,7 +59,8 @@ simpl;auto.
 Qed.
 
 Lemma Lget_app : forall (A:Set) (a:A) l i,
-Lget i (l ++ a :: nil) = if nat_eq i (length l) then Some a else Lget i l.
+Lget i (l ++ a :: nil) = if nat_beq i (length l) then Some a else Lget i l.
+Proof.
 induction l;simpl Lget;simpl length.
 intros [ | i];simpl;reflexivity.
 intros [ | i];simpl.
@@ -274,17 +156,20 @@ Qed.
 
 Theorem Tget_Tadd: forall i j a T,
        Tget i (Tadd j a T) =
-       match (i ?= j) Eq with
+       match (i ?= j) with
          Eq => PSome a
        | Lt => Tget i T
        | Gt => Tget i T
        end.
+Proof.
 intros i j.
-caseq ((i ?= j) Eq).
-intro H;rewrite (Pcompare_Eq_eq _ _ H);intros a;clear i H.
+case_eq (i ?= j).
+intro H;rewrite (Pos.compare_eq _ _ H);intros a;clear i H.
 induction j;destruct T;simpl;try (apply IHj);congruence.
+unfold Pos.compare.
 generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
+unfold Pos.compare.
 generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
 Qed.
@@ -308,7 +193,8 @@ Inductive Full : Store -> Type:=
   | F_push : forall a S, Full S -> Full (push a S).
 
 Theorem get_Full_Gt : forall S, Full S ->
-       forall i, (i ?= index S) Eq = Gt -> get i S = PNone.
+       forall i, (i ?= index S) = Gt -> get i S = PNone.
+Proof.
 intros S W;induction W.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
 unfold index,get,push;simpl contents.
@@ -335,16 +221,17 @@ Qed.
 Theorem get_push_Full :
   forall i a S, Full S ->
   get i (push a S) =
-  match (i ?= index S) Eq with
+  match (i ?= index S) with
     Eq => PSome a
   | Lt => get i S
   | Gt => PNone
 end.
+Proof.
 intros i a S F.
-caseq ((i ?= index S) Eq).
-intro e;rewrite (Pcompare_Eq_eq _ _ e).
+case_eq (i ?= index S).
+intro e;rewrite (Pos.compare_eq _ _ e).
 destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
-rewrite Pcompare_refl;reflexivity.
+rewrite Pos.compare_refl;reflexivity.
 intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
 simpl index in H;rewrite H;reflexivity.
 intro H;generalize H;clear H.
@@ -357,8 +244,9 @@ Qed.
 Lemma Full_push_compat : forall i a S, Full S ->
 forall x, get i S = PSome x ->
  get i (push a S) = PSome x.
+Proof.
 intros i a S F x H.
-caseq ((i ?= index S) Eq);intro test.
+case_eq (i ?= index S);intro test.
 rewrite (Pcompare_Eq_eq _ _ test) in H.
 rewrite (get_Full_Eq _ F) in H;congruence.
 rewrite <- H.
@@ -391,7 +279,7 @@ get i S = PSome x -> In x S F.
 induction F.
 intro i;rewrite get_empty; congruence.
 intro i;rewrite get_push_Full;trivial.
-caseq ((i ?= index S) Eq);simpl.
+case_eq (i ?= index S);simpl.
 left;congruence.
 right;eauto.
 congruence.
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index f5d452f7e..8b5e42447 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -13,7 +13,6 @@ Require Import Bool.
 
 Declare ML Module "rtauto_plugin".
 
-Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 Ltac clean:=try (simpl;congruence).
 
 Inductive form:Set:=
@@ -66,11 +65,11 @@ end.
 Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
 induction p;destruct q;simpl;clean.
 intro h;generalize (pos_eq_refl _ _ h);congruence.
-caseq (form_eq p1 q1);clean.
+case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
-caseq (form_eq p1 q1);clean.
+case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
-caseq (form_eq p1 q1);clean.
+case_eq (form_eq p1 q1);clean.
 intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
 Qed.
 
@@ -260,7 +259,7 @@ induction p;intros hyps F gl.
 
 (* cas Axiom *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f nth_f e;rewrite <- (form_eq_refl e).
 apply project with p;trivial.
 
@@ -273,10 +272,10 @@ apply IHp;try constructor;trivial.
 
 (* Cas Arrow_Elim *)
 Focus 1.
-simpl check_proof;caseq (get p hyps);clean.
-intros f ef;caseq (get p0 hyps);clean.
+simpl check_proof;case_eq (get p hyps);clean.
+intros f ef;case_eq (get p0 hyps);clean.
 intros f0 ef0;destruct f0;clean.
-caseq (form_eq f f0_1);clean.
+case_eq (form_eq f f0_1);clean.
 simpl;intros e check_p1.
 generalize  (project  F ef) (project  F ef0)
 (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
@@ -288,10 +287,10 @@ auto.
 
 (* cas Arrow_Destruct *)
 Focus 1.
-simpl;caseq (get p1 hyps);clean.
+simpl;case_eq (get p1 hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
-caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
+case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
 intros check_p1 check_p2.
 generalize (project F ef)
 (IHp1 (hyps \ f1_2 =>> f2 \ f1_1)
@@ -302,7 +301,7 @@ simpl;apply compose3;auto.
 
 (* Cas False_Elim *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 intros _; generalize (project F ef).
 apply compose1;apply False_ind.
@@ -310,13 +309,13 @@ apply compose1;apply False_ind.
 (* Cas And_Intro *)
 Focus 1.
 simpl;destruct gl;clean.
-caseq (check_proof hyps gl1 p1);clean.
+case_eq (check_proof hyps gl1 p1);clean.
 intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
 apply compose2 ;simpl;auto.
 
 (* cas And_Elim *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 intro check_p;generalize  (project F ef)
 (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p).
@@ -324,7 +323,7 @@ simpl;apply compose2;intros [h1 h2];auto.
 
 (* cas And_Destruct *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
 intro H;generalize  (project F ef)
@@ -346,9 +345,9 @@ apply compose1;simpl;auto.
 
 (* cas Or_elim *)
 Focus 1.
-simpl;caseq (get p1 hyps);clean.
+simpl;case_eq (get p1 hyps);clean.
 intros f ef;destruct f;clean.
-caseq (check_proof (hyps \ f1) gl p2);clean.
+case_eq (check_proof (hyps \ f1) gl p2);clean.
 intros check_p1 check_p2;generalize (project F ef)
 (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1)
 (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2);
@@ -356,7 +355,7 @@ simpl;apply compose3;simpl;intro h;destruct h;auto.
 
 (* cas Or_Destruct *)
 Focus 1.
-simpl;caseq (get p hyps);clean.
+simpl;case_eq (get p hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
 intro check_p0;generalize (project F ef)
@@ -367,7 +366,7 @@ apply compose2;auto.
 
 (* cas Cut *)
 Focus 1.
-simpl;caseq (check_proof hyps f p1);clean.
+simpl;case_eq (check_proof hyps f p1);clean.
 intros check_p1 check_p2;
 generalize (IHp1 hyps F f check_p1)
 (IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
@@ -375,7 +374,7 @@ simpl; apply compose2;auto.
 Qed.
 
 Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
-intros gl prf;caseq (check_proof empty gl prf);intro check_prf.
+intros gl prf;case_eq (check_proof empty gl prf);intro check_prf.
 change (interp_ctx empty F_empty [[gl]]) ;
 apply interp_proof with prf;assumption.
 trivial.
diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v
index 4a0beb3fa..3cd9d4d3e 100644
--- a/plugins/setoid_ring/Cring_initial.v
+++ b/plugins/setoid_ring/Cring_initial.v
@@ -147,7 +147,7 @@ Ltac rsimpl := simpl;  set_cring_notations.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
  gen_phiZ1
-    match (x ?= y)%positive Eq with
+    match (x ?= y)%positive with
     | Eq => Z0
     | Lt => Zneg (y - x)
     | Gt => Zpos (x - y)
@@ -155,12 +155,11 @@ Ltac rsimpl := simpl;  set_cring_notations.
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
-  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
-  generalize (Pminus_mask_Gt y x).
-  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
-  rewrite <- Pcompare_antisym in H1.
-  destruct ((x ?= y)%positive Eq).
-  cring_rewrite H;trivial. cring_rewrite cring_opp_def;gen_reflexivity.
+  assert (H0 := Pminus_mask_Gt x y). unfold Pgt in H0.
+  assert (H1 := Pminus_mask_Gt y x). unfold Pgt in H1.
+  rewrite Pos.compare_antisym in H1.
+  destruct (Pos.compare_spec x y) as [H|H|H].
+  subst. cring_rewrite cring_opp_def;gen_reflexivity.
   destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
   unfold Pminus; cring_rewrite Heq1;rewrite <- Heq2.
   cring_rewrite ARgen_phiPOS_add;simpl;norm.
@@ -182,8 +181,7 @@ Ltac rsimpl := simpl;  set_cring_notations.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
-  replace Eq with (CompOpp Eq);trivial.
-  rewrite <- Pcompare_antisym;simpl.
+  rewrite Pos.compare_antisym;simpl.
   cring_rewrite match_compOpp.
   cring_rewrite cring_add_comm.
   apply gen_phiZ1_add_pos_neg.
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d97238343..29d7ee333 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -779,7 +779,7 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
 Proof.
   intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
    case (PExpr_eq e1 e2); simpl; auto; intros H.
-  case_eq ((p1 ?= p2)%positive Eq);intros;simpl.
+  case_eq ((p1 ?= p2)%positive);intros;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
   rewrite (Pcompare_Eq_eq _ _ H0).
   rewrite H by trivial. ring [ (morph1 CRmorph)].
@@ -791,7 +791,7 @@ Proof.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
   rewrite H;trivial.
    change (ZtoN
-     match (p1 ?= p1 - p2)%positive Eq with
+     match (p1 ?= p1 - p2)%positive with
      | Eq => 0
      | Lt => Zneg (p1 - p2 - p1)
      | Gt => Zpos (p1 - (p1 - p2))
@@ -1805,25 +1805,24 @@ Lemma gen_phiPOS_inj : forall x y,
   x = y.
 intros x y.
 repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
-ElimPcompare x y; intro.
+case (Pos.compare_spec x y).
+ intros.
+   trivial.
  intros.
-   apply Pcompare_Eq_eq; trivial.
- intro.
    elim gen_phiPOS_not_0 with (y - x)%positive.
    apply add_inj_r with x.
    symmetry  in |- *.
    rewrite (ARadd_0_r Rsth ARth) in |- *.
    rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
    rewrite Pplus_minus in |- *; trivial.
-   change Eq with (CompOpp Eq) in |- *.
-   rewrite <- Pcompare_antisym in |- *; trivial.
-   rewrite H in |- *; trivial.
- intro.
+   now apply Pos.lt_gt.
+ intros.
    elim gen_phiPOS_not_0 with (x - y)%positive.
    apply add_inj_r with y.
    rewrite (ARadd_0_r Rsth ARth) in |- *.
    rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
    rewrite Pplus_minus in |- *; trivial.
+   now apply Pos.lt_gt.
 Qed.
 
 
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index cd59b7cb6..86fada82a 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -172,7 +172,7 @@ Section ZMORPHISM.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
  gen_phiZ1
-    match (x ?= y)%positive Eq with
+    match (x ?= y)%positive with
     | Eq => Z0
     | Lt => Zneg (y - x)
     | Gt => Zpos (x - y)
@@ -180,20 +180,14 @@ Section ZMORPHISM.
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
-  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
-  generalize (Pminus_mask_Gt y x).
-  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
-  rewrite <- Pcompare_antisym in H1.
-  destruct ((x ?= y)%positive Eq).
-  rewrite H;trivial. rewrite (Ropp_def Rth);rrefl.
-  destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+  case Pos.compare_spec; intros H; simpl.
+  rewrite H. rewrite (Ropp_def Rth);rrefl.
+  rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
   rewrite (ARgen_phiPOS_add ARth);simpl;norm.
   rewrite (Ropp_def Rth);norm.
-  destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+  rewrite <- (Pos.sub_add x y H) at 2.
   rewrite (ARgen_phiPOS_add ARth);simpl;norm.
-  add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm.
+  add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
  Qed.
 
  Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
@@ -207,8 +201,7 @@ Section ZMORPHISM.
   induction x;destruct y;simpl;norm.
   apply (ARgen_phiPOS_add ARth).
   apply gen_phiZ1_add_pos_neg.
-  replace Eq with (CompOpp Eq);trivial.
-  rewrite <- Pcompare_antisym;simpl.
+  rewrite Pos.compare_antisym.
   rewrite match_compOpp.
   rewrite (Radd_comm Rth).
   apply gen_phiZ1_add_pos_neg.
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v
index 38a300f71..f94ad9b0f 100644
--- a/plugins/setoid_ring/Ring2_initial.v
+++ b/plugins/setoid_ring/Ring2_initial.v
@@ -147,7 +147,7 @@ Ltac rsimpl := simpl;  set_ring_notations.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
  gen_phiZ1
-    match (x ?= y)%positive Eq with
+    match (x ?= y)%positive with
     | Eq => Z0
     | Lt => Zneg (y - x)
     | Gt => Zpos (x - y)
@@ -155,12 +155,11 @@ Ltac rsimpl := simpl;  set_ring_notations.
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
-  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
-  generalize (Pminus_mask_Gt y x).
-  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
-  rewrite <- Pcompare_antisym in H1.
-  destruct ((x ?= y)%positive Eq).
-  ring_rewrite H;trivial. ring_rewrite ring_opp_def;gen_reflexivity.
+  assert (H0 := Pminus_mask_Gt x y). unfold Pos.gt in H0.
+  assert (H1 := Pminus_mask_Gt y x). unfold Pos.gt in H1.
+  rewrite Pos.compare_antisym in H1.
+  destruct (Pos.compare_spec x y) as [H|H|H].
+  subst. ring_rewrite ring_opp_def;gen_reflexivity.
   destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
   unfold Pminus; ring_rewrite Heq1;rewrite <- Heq2.
   ring_rewrite ARgen_phiPOS_add;simpl;norm.
@@ -183,7 +182,7 @@ Ltac rsimpl := simpl;  set_ring_notations.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
   replace Eq with (CompOpp Eq);trivial.
-  rewrite <- Pcompare_antisym;simpl.
+  rewrite Pos.compare_antisym;simpl.
   ring_rewrite match_compOpp.
   ring_rewrite ring_add_comm.
   apply gen_phiZ1_add_pos_neg.
diff --git a/plugins/setoid_ring/Ring2_polynom.v b/plugins/setoid_ring/Ring2_polynom.v
index 6fa0f200b..fdf5ca545 100644
--- a/plugins/setoid_ring/Ring2_polynom.v
+++ b/plugins/setoid_ring/Ring2_polynom.v
@@ -65,7 +65,7 @@ Instance equalityb_coef : Equalityb C :=
   match P, P' with
   | Pc c, Pc c' => c =? c'
   | PX P i n Q, PX P' i' n' Q' =>
-    match Pcompare i i' Eq, Pcompare n n' Eq with
+    match Pos.compare i i', Pos.compare n n' with
     | Eq, Eq => if Peq P P' then Peq Q Q' else false
     | _,_ => false
     end
@@ -80,7 +80,7 @@ Instance equalityb_pol : Equalityb Pol :=
   match P with
   | Pc c => if c =? cO then Q else PX P i n Q 
   | PX P' i' n' Q' => 
-       match Pcompare i i' Eq with
+       match Pos.compare i i' with
         | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q
         | _ => PX P i n Q
        end
@@ -122,7 +122,7 @@ Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
   match Q with
   | Pc c => mkPX P i n Q
   | PX P' i' n' Q' => 
-      match Pcompare i i' Eq with
+      match Pos.compare i i' with
       | (* i > i' *)
         Gt => mkPX P i n Q
       | (* i < i' *)
@@ -225,20 +225,14 @@ Definition Psub(P P':Pol):= P ++ (--P').
     (P =? P') = true -> forall l, P@l == P'@ l.
  Proof.
   induction P;destruct P';simpl;intros;try discriminate;trivial. apply ring_morphism_eq.
- apply Ceqb_eq ;trivial.
-
-  assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2).
-   simpl in H1. destruct (Peq P2 P'1). simpl in H2; destruct (Peq P3 P'2).
-  ring_rewrite (H1);trivial . ring_rewrite (H2);trivial. 
-assert (H3 := Pcompare_Eq_eq p p1);
- destruct ((p ?= p1)%positive Eq);
-assert (H4 := Pcompare_Eq_eq p0 p2);
-destruct ((p0 ?= p2)%positive Eq); try (discriminate H).
- ring_rewrite H3;trivial. ring_rewrite H4;trivial. rrefl.
- destruct ((p ?= p1)%positive Eq); destruct ((p0 ?= p2)%positive Eq);
- try (discriminate H).
- destruct ((p ?= p1)%positive Eq); destruct ((p0 ?= p2)%positive Eq);
- try (discriminate H). 
+  apply Ceqb_eq ;trivial.
+  destruct (Pos.compare_spec p p1); try discriminate H.
+  destruct (Pos.compare_spec p0 p2); try discriminate H.
+  assert (H1' := IHP1 P'1);assert (H2' := IHP2 P'2).
+  simpl in H1'. destruct (Peq P2 P'1); try discriminate H.
+  simpl in H2'. destruct (Peq P3 P'2); try discriminate H.
+  ring_rewrite (H1');trivial . ring_rewrite (H2');trivial.
+  subst. rrefl.
  Qed.
 
  Lemma Pphi0 : forall l, P0@l == 0.
@@ -262,13 +256,15 @@ destruct ((p0 ?= p2)%positive Eq); try (discriminate H).
   assert (H := ring_morphism_eq  c cO). simpl; case_eq (Ceqb c cO);simpl;try rrefl.
 intros.
   ring_rewrite H. ring_rewrite ring_morphism0.
-  rsimpl. apply Ceqb_eq. trivial. assert (H1 := Pcompare_Eq_eq i p);
-destruct ((i ?= p)%positive Eq).
-  assert (H := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. 
-  ring_rewrite H. 
-  ring_rewrite Pphi0. rsimpl. ring_rewrite Pplus_comm. ring_rewrite pow_pos_Pplus;rsimpl.
-ring_rewrite H1;trivial. rrefl. trivial. intros. simpl. rrefl. simpl. rrefl.
- simpl. rrefl.
+  rsimpl. apply Ceqb_eq. trivial.
+  case Pos.compare_spec; intros; subst.
+  assert (H := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl.
+  ring_rewrite H; trivial.
+  ring_rewrite Pphi0. rsimpl. ring_rewrite Pplus_comm.
+  ring_rewrite pow_pos_Pplus;rsimpl; trivial.
+  rrefl.
+  rrefl.
+  rrefl.
  Qed.
 
 Ltac Esimpl :=
@@ -337,7 +333,7 @@ Lemma PaddXPX: forall P i n Q,
   match Q with
   | Pc c => mkPX P i n Q
   | PX P' i' n' Q' => 
-      match Pcompare i i' Eq with
+      match Pos.compare i i' with
       | (* i > i' *)
         Gt => mkPX P i n Q
       | (* i < i' *)
@@ -365,18 +361,16 @@ Lemma PaddX_ok2 : forall P2,
 induction P2;ring_simpl;intros. split. intros. apply PaddCl_ok.
  induction P.  unfold PaddX. intros. ring_rewrite mkPX_ok.
  ring_simpl. rsimpl.
-intros. ring_simpl. assert (H := Pcompare_Eq_eq k p);
- destruct ((k ?= p)%positive Eq).
+intros. ring_simpl.
+ case Pos.compare_spec; intros; subst.
  assert (H1 := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2.
-ring_rewrite H; trivial. rewrite H1. rrefl.
+ rewrite H1. rrefl.
 ring_simpl. ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2.
  rewrite Pplus_comm in H1.
 rewrite H1. 
 ring_rewrite pow_pos_Pplus.  Esimpl2.
-rewrite H; trivial. rrefl.
 ring_rewrite mkPX_ok. ring_rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1.
 rewrite H1.  Esimpl2. ring_rewrite pow_pos_Pplus. Esimpl2.
-rewrite H; trivial. rrefl.
 ring_rewrite mkPX_ok. ring_rewrite IHP2. Esimpl2.
 ring_rewrite (ring_add_comm  (P2 @ l * pow_pos Rr (nth 0 p l) p0) 
                              ([c] * pow_pos Rr (nth 0 k l) n)).
@@ -388,17 +382,16 @@ split. intros. ring_rewrite H0. ring_rewrite H1.
 Esimpl2.
 induction P. unfold PaddX. intros. ring_rewrite mkPX_ok. ring_simpl. rrefl.
 intros. ring_rewrite PaddXPX. 
-assert (H3 := Pcompare_Eq_eq k p1);
- destruct ((k ?= p1)%positive Eq).
+case Pos.compare_spec; intros; subst.
 assert (H4 := ZPminus_spec n p2);destruct (ZPminus n p2). 
 ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. Esimpl2.
-rewrite H4. rewrite H3;trivial. rrefl.
-ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2. rewrite H3;trivial.
+rewrite H4. rrefl.
+ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2.
 rewrite Pplus_comm in H4.
 rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2.
 ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. 
 ring_rewrite mkPX_ok.
- Esimpl2. rewrite H3;trivial.
+ Esimpl2.
  rewrite Pplus_comm in H4.
 rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2.
 ring_rewrite mkPX_ok. ring_simpl. ring_rewrite IHP2. Esimpl2.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index abaa312e1..b722a31b6 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -104,12 +104,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
@@ -435,7 +435,7 @@ Section MakeRingPol.
             CFactor P c
    | 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 c M1 in
                  (mkPinj j1 R, mkPinj j1 S)
       | Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in
@@ -449,7 +449,7 @@ Section MakeRingPol.
              let (R2, S2) := MFactor Q1 c 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 c (mkZmon xH M1) in
                  (mkPX R1 i Q1, S1)
       | Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in
@@ -552,10 +552,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);
@@ -947,8 +947,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    generalize (Mcphi_ok P c (jump i l)); case CFactor.
    intros R1 Q1 HH; rewrite HH; Esimpl.
      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 (c, M) (jump j l)); case (MFactor P c M);
         simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
        generalize (Hrec (c, (zmon (j -i) M)) (jump i l));
@@ -987,8 +987,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
      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 (c, mkZmon xH M1) l); case (MFactor P2 c (mkZmon xH M1));
         simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
        rewrite H; rewrite mkPX_ok; rsimpl.