ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

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

17 files changed, 553 insertions, 857 deletions

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 06822ae16..8e234db74 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -21,17 +21,17 @@ Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
 
 Lemma nat_morph_N :
    semi_morph 0 1 plus mult (eq (A:=nat))
-          0%N 1%N N.add N.mul N.eqb nat_of_N.
+          0%N 1%N N.add N.mul N.eqb N.to_nat.
 Proof.
   constructor;trivial.
-  exact nat_of_Nplus.
-  exact nat_of_Nmult.
+  exact N2Nat.inj_add.
+  exact N2Nat.inj_mul.
   intros x y H. apply N.eqb_eq in H. now subst.
 Qed.
 
 Ltac natcst t :=
   match isnatcst t with
-    true => constr:(N_of_nat t)
+    true => constr:(N.of_nat t)
   | _ => constr:InitialRing.NotConstant
   end.
 
diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v
index 7128280a0..2e317d784 100644
--- a/plugins/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
@@ -6,11 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Set Implicit Arguments.
 Require Import BinPos.
 Require Export List.
-Require Export ListTactics.
-Open Local Scope positive_scope.
+Set Implicit Arguments.
+Local Open Scope positive_scope.
 
 Section MakeBinList.
  Variable A : Type.
@@ -18,76 +17,64 @@ Section MakeBinList.
 
  Fixpoint jump (p:positive) (l:list A) {struct p} : list A :=
   match p with
-  | xH => tail l
+  | xH => tl l
   | xO p => jump p (jump p l)
-  | xI p  => jump p (jump p (tail l))
+  | xI p  => jump p (jump p (tl l))
   end.
 
  Fixpoint nth (p:positive) (l:list A) {struct p} : A:=
   match p with
   | xH => hd default l
   | xO p => nth p (jump p l)
-  | xI p => nth p (jump p (tail l))
+  | xI p => nth p (jump p (tl l))
   end.
 
- Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
+ Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l).
  Proof.
-  induction j;simpl;intros.
-  repeat rewrite IHj;trivial.
-  repeat rewrite IHj;trivial.
-  trivial.
+  induction j;simpl;intros; now rewrite ?IHj.
  Qed.
 
- Lemma jump_Psucc : forall j l,
-  (jump (Psucc j) l) = (jump 1 (jump j l)).
+ Lemma jump_succ : forall j l,
+  jump (Pos.succ j) l = jump 1 (jump j l).
  Proof.
   induction j;simpl;intros.
-  repeat rewrite IHj;simpl;repeat rewrite jump_tl;trivial.
-  repeat rewrite jump_tl;trivial.
-  trivial.
+  - rewrite !IHj; simpl; now rewrite !jump_tl.
+  - now rewrite !jump_tl.
+  - trivial.
  Qed.
 
- Lemma jump_Pplus : forall i j l,
-  (jump (i + j) l) = (jump i (jump j l)).
+ Lemma jump_add : forall i j l,
+  jump (i + j) l = jump i (jump j l).
  Proof.
-  induction i;intros.
-  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat rewrite IHi.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat rewrite IHi;trivial.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial.
+  induction i using Pos.peano_ind; intros.
+  - now rewrite Pos.add_1_l, jump_succ.
+  - now rewrite Pos.add_succ_l, !jump_succ, IHi.
  Qed.
 
- Lemma jump_Pdouble_minus_one : forall i l,
-  (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)).
+ Lemma jump_pred_double : forall i l,
+  jump (Pos.pred_double i) (tl l) = jump i (jump i l).
  Proof.
   induction i;intros;simpl.
-  repeat rewrite jump_tl;trivial.
-  rewrite IHi. do 2 rewrite <- jump_tl;rewrite IHi;trivial.
-  trivial.
+  - now rewrite !jump_tl.
+  - now rewrite IHi, <- 2 jump_tl, IHi.
+  - trivial.
  Qed.
 
-
- Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l).
+ Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l).
  Proof.
   induction p;simpl;intros.
-  rewrite <-jump_tl;rewrite IHp;trivial.
-  rewrite <-jump_tl;rewrite IHp;trivial.
-  trivial.
+  - now rewrite <-jump_tl, IHp.
+  - now rewrite <-jump_tl, IHp.
+  - trivial.
  Qed.
 
- Lemma nth_Pdouble_minus_one :
-  forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
+ Lemma nth_pred_double :
+  forall p l, nth (Pos.pred_double p) (tl l) = nth p (jump p l).
  Proof.
   induction p;simpl;intros.
-  repeat rewrite jump_tl;trivial.
-  rewrite jump_Pdouble_minus_one.
-  repeat rewrite <- jump_tl;rewrite IHp;trivial.
-  trivial.
+  - now rewrite !jump_tl.
+  - now rewrite jump_pred_double, <- !jump_tl, IHp.
+  - trivial.
  Qed.
 
 End MakeBinList.
-
-
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 3d6e53fcd..592efbf6d 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -42,10 +42,9 @@ Section cring.
 Context {R:Type}`{Rr:Cring R}.
 
 Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
-intros. apply mk_reqe;intros. 
-rewrite H. rewrite H0. reflexivity.
-rewrite H. rewrite H0. reflexivity.
- rewrite H. reflexivity. Defined.
+Proof.
+intros. apply mk_reqe; solve_proper.
+Defined.
 
 Lemma cring_almost_ring_theory:
    almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
@@ -64,11 +63,11 @@ rewrite ring_sub_def ; reflexivity. Defined.
 
 Lemma cring_morph:
   ring_morph  zero one _+_ _*_ _-_ -_ _==_
-             0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+             0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
              Ncring_initial.gen_phiZ.
 intros. apply mkmorph ; intros; simpl; try reflexivity.
 rewrite Ncring_initial.gen_phiZ_add; reflexivity.
-rewrite ring_sub_def. unfold Zminus. rewrite Ncring_initial.gen_phiZ_add.
+rewrite ring_sub_def. unfold Z.sub. rewrite Ncring_initial.gen_phiZ_add.
 rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
 rewrite Ncring_initial.gen_phiZ_mul; reflexivity.
 rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
@@ -80,7 +79,7 @@ Lemma cring_power_theory :
 intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
 
 Lemma cring_div_theory: 
-  div_theory _==_ Zplus Zmult Ncring_initial.gen_phiZ Z.quotrem.
+  div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem.
 intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
 simpl.   apply ring_setoid. Defined.
 
@@ -102,7 +101,7 @@ Ltac cring_gen :=
                         ring_setoid
                         cring_eq_ext
                         cring_almost_ring_theory
-                        Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+                        Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
                         Ncring_initial.gen_phiZ
                         cring_morph
                         N
@@ -126,7 +125,7 @@ Ltac cring:=
   cring_compute.
 
 Instance Zcri: (Cring (Rr:=Zr)).
-red. exact Zmult_comm. Defined.
+red. exact Z.mul_comm. Defined.
 
 (* Cring_simplify *)
 
@@ -136,7 +135,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp :=
     match lexpr with
       | ?e::?le =>
         let t := constr:(@Ring_polynom.norm_subst
-          Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Z.quotrem O nil e) in
+          Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e) in
         let te := 
           constr:(@Ring_polynom.Pphi_dev
             _ 0 1 _+_ _*_ _-_ -_ 
@@ -149,7 +148,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp :=
         let t':= fresh "t" in
         pose (t' := nft);
         assert (eq1 : t = t');
-        [vm_cast_no_check (refl_equal t')|
+        [vm_cast_no_check (eq_refl t')|
         let eq2 := fresh "ring" in
         assert (eq2:(@Ring_polynom.PEeval
           _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
@@ -159,7 +158,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp :=
             ring_setoid
             cring_eq_ext
             cring_almost_ring_theory
-            Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+            Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
             Ncring_initial.gen_phiZ
             cring_morph
             N
@@ -169,7 +168,7 @@ Ltac cring_simplify_aux lterm fv lexpr hyp :=
             Z.quotrem
             cring_div_theory
             get_signZ get_signZ_th
-            O nil fv I nil (refl_equal nil) );
+            O nil fv I nil (eq_refl nil) );
           intro eq3; apply eq3; reflexivity|
               match hyp with
                 | 1%nat => rewrite eq2
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index da42bbd95..056203926 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -447,7 +447,7 @@ Ltac prove_field_eqn ope FLD fv expr :=
   pose (res' := res);
   let lemma := get_L1 FLD in
   let lemma :=
-    constr:(lemma O fv List.nil expr' res' I List.nil (refl_equal _)) in
+    constr:(lemma O fv List.nil expr' res' I List.nil (eq_refl _)) in
   let ty := type of lemma in
   let lhs := match ty with
     forall _, ?lhs=_ -> _ => lhs
@@ -487,7 +487,7 @@ Ltac reduce_field_expr ope kont FLD fv expr :=
   kont c.
 
 (* Hack to let a Ltac return a term in the context of a primitive tactic *)
-Ltac return_term x := generalize (refl_equal x).
+Ltac return_term x := generalize (eq_refl x).
 Ltac get_term :=
   match goal with
   | |- ?x = _ -> _ => x
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 40138526d..17595639b 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Ring.
-Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List.
+Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms.
 Require Import ZArith_base.
 (*Require Import Omega.*)
 Set Implicit Arguments.
@@ -27,7 +27,7 @@ Section MakeFieldPol.
  Notation "x == y" := (req x y) (at level 70, no associativity).
 
  (* Equality properties *)
- Variable Rsth : Setoid_Theory R req.
+ Variable Rsth : Equivalence req.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
  Variable SRinv_ext : forall p q, p == q ->  / p == / q.
 
@@ -75,7 +75,6 @@ Qed.
 
 
  (* Useful tactics *)
-  Add Setoid R req Rsth as R_set1.
   Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
   Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
@@ -116,6 +115,7 @@ Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi
 (* add abstract semi-ring to help with some proofs *)
 Add Ring Rring : (ARth_SRth ARth).
 
+Local Hint Extern 2 (_ == _) => f_equiv.
 
 (* additional ring properties *)
 
@@ -135,6 +135,7 @@ Qed.
   ***************************************************************************)
 
 Theorem rdiv_simpl: forall p q, ~ q == 0 ->  q * (p / q) == p.
+Proof.
 intros p q H.
 rewrite rdiv_def in |- *.
 transitivity (/ q * q * p); [  ring | idtac ].
@@ -142,35 +143,32 @@ rewrite rinv_l in |- *; auto.
 Qed.
 Hint Resolve rdiv_simpl .
 
-Theorem SRdiv_ext:
- forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 ->  p1 / q1 == p2 / q2.
-intros p1 p2 H q1 q2 H0.
+Instance SRdiv_ext: Proper (req ==> req ==> req) rdiv.
+Proof.
+intros p1 p2 Ep q1 q2 Eq.
 transitivity (p1 * / q1); auto.
 transitivity (p2 * / q2); auto.
 Qed.
-Hint Resolve SRdiv_ext .
-
- Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed.
+Hint Resolve SRdiv_ext.
 
 Lemma rmul_reg_l : forall p q1 q2,
   ~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
-intros.
-rewrite <- (@rdiv_simpl q1 p) in |- *; trivial.
-rewrite <- (@rdiv_simpl q2 p) in |- *; trivial.
-repeat rewrite rdiv_def in |- *.
-repeat rewrite (ARmul_assoc ARth) in |- *.
-auto.
+Proof.
+intros p q1 q2 H EQ.
+rewrite <- (@rdiv_simpl q1 p) by trivial.
+rewrite <- (@rdiv_simpl q2 p) by trivial.
+rewrite !rdiv_def, !(ARmul_assoc ARth).
+now rewrite EQ.
 Qed.
 
 Theorem field_is_integral_domain : forall r1 r2,
   ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
 Proof.
-red in |- *; intros.
-apply H0.
+intros r1 r2 H1 H2. contradict H2.
 transitivity (1 * r2); auto.
 transitivity (/ r1 * r1 * r2); auto.
-rewrite <- (ARmul_assoc ARth) in |- *.
-rewrite H1 in |- *.
+rewrite <- (ARmul_assoc ARth).
+rewrite H2.
 apply ARmul_0_r with (1 := Rsth) (2 := ARth).
 Qed.
 
@@ -205,12 +203,12 @@ Proof.
 intros r1 r2 r3 r4 H H0.
 assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
 apply rmul_reg_l with (r2 * r4); trivial.
-rewrite rdiv_simpl in |- *; trivial.
-rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+rewrite rdiv_simpl; trivial.
+rewrite (ARdistr_r Rsth Reqe ARth).
 apply (Radd_ext Reqe).
- transitivity (r2 * (r1 / r2) * r4); [  ring | auto ].
- transitivity (r2 * (r4 * (r3 / r4))); auto.
-   transitivity (r2 * r3); auto.
+- transitivity (r2 * (r1 / r2) * r4); [  ring | auto ].
+- transitivity (r2 * (r4 * (r3 / r4))); auto.
+  transitivity (r2 * r3); auto.
 Qed.
 
 
@@ -235,25 +233,26 @@ apply (Radd_ext Reqe).
 Qed.
 
 Theorem rdiv5: forall r1 r2,  - (r1 / r2) == - r1 / r2.
+Proof.
 intros r1 r2.
 transitivity (- (r1 * / r2)); auto.
 transitivity (- r1 * / r2); auto.
 Qed.
 Hint Resolve rdiv5 .
 
-Theorem rdiv3:
- forall r1 r2 r3 r4,
+Theorem rdiv3 r1 r2 r3 r4 :
  ~ r2 == 0 ->
  ~ r4 == 0 ->
  r1 / r2 - r3 / r4 == (r1 * r4 -  r3 * r2) / (r2 * r4).
-intros r1 r2 r3 r4 H H0.
+Proof.
+intros H2 H4.
 assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
 transitivity (r1 / r2 + - (r3 / r4)); auto.
 transitivity (r1 / r2 + - r3 / r4); auto.
-transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto.
+transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)).
 apply rdiv2; auto.
-apply SRdiv_ext; auto.
-transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
+f_equiv.
+transitivity (r1 * r4 + - (r3 * r2)); auto.
 Qed.
 
 
@@ -410,14 +409,7 @@ Qed.
 Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph.
 intros x y H [|p];simpl;auto. apply pow_morph;trivial.
 Qed.
-(*
-Lemma rpow_morph : forall x y n, x == y ->rpow x (Cp_phi n) == rpow y (Cp_phi n).
-Proof.
-  intros; repeat rewrite pow_th.(rpow_pow_N).
-  destruct n;simpl. apply eq_refl.
-  induction p;simpl;try rewrite IHp;try rewrite H; apply eq_refl.
-Qed.
-*)
+
 Theorem PExpr_eq_semi_correct:
  forall l e1 e2, PExpr_eq e1 e2 = true ->  NPEeval l e1 == NPEeval l e2.
 intros l e1; elim e1.
@@ -705,10 +697,10 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
          end
        end
   | PEpow e3 N0 => None
-  | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2)
+  | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pos.mul p3 p2)
   | _ =>
      if  PExpr_eq e1 e2 then
-         match Zminus (Zpos p1) (Zpos p2) with
+         match Z.pos_sub p1 p2 with
           | Zpos p => Some (Npos p, PEc cI)
           | Z0 => Some (N0, PEc cI)
           | Zneg p => Some (N0, NPEpow e2 (Npos p))
@@ -719,21 +711,19 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
  Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end.
  Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end.
 
- Notation pow_pos_plus :=  (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext)
-                        ARth.(ARmul_comm) ARth.(ARmul_assoc)).
+ Notation pow_pos_add :=
+   (Ring_theory.pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
 
- Lemma Z_pos_sub_gt : forall p q, (p > q)%positive ->
+ Lemma Z_pos_sub_gt p q : (p > q)%positive ->
   Z.pos_sub p q = Zpos (p - q).
- Proof.
-  intros. apply Z.pos_sub_gt. now apply Pos.gt_lt.
- Qed.
+ Proof. intros; now apply Z.pos_sub_gt, Pos.gt_lt. Qed.
 
  Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
 
  Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
   match
       (if  PExpr_eq e1 e2 then
-         match Zminus (Zpos p1) (Zpos p2) with
+         match Z.sub (Zpos p1) (Zpos p2) with
           | Zpos p => Some (Npos p, PEc cI)
           | Z0 => Some (N0, PEc cI)
           | Zneg p => Some (N0, NPEpow e2 (Npos p))
@@ -750,33 +740,28 @@ Proof.
   intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
    case (PExpr_eq e1 e2); simpl; auto; intros H.
   rewrite Z.pos_sub_spec.
-  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)].
-  fold (p2 - p1 =? 1)%positive.
-  fold (NPEpow e2 (Npos (p2 - p1))).
-  rewrite NPEpow_correct;simpl.
-  repeat rewrite pow_th.(rpow_pow_N);simpl.
-  rewrite H;trivial. split. 2:refine (refl_equal _).
-  rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial.
-  repeat rewrite pow_th.(rpow_pow_N);simpl.
-  rewrite H;trivial.
-   change (Z.pos_sub p1 (p1-p2)) with (Zpos p1 - Zpos (p1 -p2))%Z.
-  replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
-  split.
-  repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
-  rewrite Zplus_assoc, Z.add_opp_diag_r. simpl.
-  ring [ (morph1 CRmorph)].
- assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _).
- apply Zplus_gt_reg_l with (Zpos p2).
- rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
- apply Zplus_gt_compat_r. refine (refl_equal _).
- simpl. now simpl_pos_sub.
+  case Pos.compare_spec;intros;simpl.
+  - repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:reflexivity.
+    subst. rewrite H by trivial. ring [ (morph1 CRmorph)].
+  - fold (p2 - p1 =? 1)%positive.
+    fold (NPEpow e2 (Npos (p2 - p1))).
+    rewrite NPEpow_correct;simpl.
+    repeat rewrite pow_th.(rpow_pow_N);simpl.
+    rewrite H;trivial. split. 2:reflexivity.
+    rewrite <- pow_pos_add. now rewrite Pos.add_comm, Pos.sub_add.
+  - repeat rewrite pow_th.(rpow_pow_N);simpl.
+    rewrite H;trivial.
+    rewrite Z.pos_sub_gt by now apply Pos.sub_decr.
+    replace (p1 - (p1 - p2))%positive with p2;
+    [| rewrite Pos.sub_sub_distr, Pos.add_comm;
+       auto using Pos.add_sub, Pos.sub_decr ].
+    split.
+    simpl. ring [ (morph1 CRmorph)].
+    now apply Z.lt_gt, Pos.sub_decr.
 Qed.
 
 Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
-induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_plus;simpl.
+induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_add;simpl.
 ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto.
 Qed.
 
@@ -808,8 +793,9 @@ destruct n.
         (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
         pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) *
         NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H.
-   rewrite <- pow_pos_plus. rewrite Pplus_minus.
-   split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
+   rewrite <- pow_pos_add.
+   rewrite Pos.add_comm, Pos.sub_add by (now apply Z.gt_lt in H4).
+   split. symmetry;apply ARth.(ARmul_assoc). reflexivity.
    repeat rewrite pow_th.(rpow_pow_N);simpl.
    intros (H1,H2) (H3,H4).
    simpl_pos_sub. simpl in H1, H3.
@@ -822,15 +808,15 @@ destruct n.
                 (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) ==
              pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) *
                 NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0.
-  rewrite <- pow_pos_plus.
+  rewrite <- pow_pos_add.
   replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive.
  rewrite NPEmul_correct. simpl;ring.
   assert
      (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
  change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
- rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)).
+ rewrite <- Z.add_assoc. rewrite (Z.add_assoc  (- Zpos p4)).
  simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
- unfold Zminus, Zopp in H0. simpl in H0.
+ unfold Z.sub, Z.opp in H0. simpl in H0.
   simpl_pos_sub. inversion H0; trivial.
  simpl. repeat rewrite pow_th.(rpow_pow_N).
  intros H1 (H2,H3). simpl_pos_sub.
@@ -875,7 +861,7 @@ Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit :
                     (NPEmul (common r1) (common r2))
                     (right r2)
   | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2
-  | PEpow e3 (Npos p3) => split_aux e3 (Pmult p3 p) e2
+  | PEpow e3 (Npos p3) => split_aux e3 (Pos.mul p3 p) e2
   | _ =>
        match isIn e1 p e2 xH with
        | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
@@ -903,7 +889,8 @@ Proof.
      repeat rewrite pow_th.(rpow_pow_N);simpl).
   intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
   intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
-  rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
+  apply Z.gt_lt in Hgt.
+  now rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add.
   simpl;intros. repeat rewrite NPEmul_correct;simpl.
   rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
 Qed.
@@ -1319,9 +1306,9 @@ apply Fnorm_crossproduct; trivial.
 match goal with
  [ |- NPEeval l ?x == NPEeval l ?y] =>
     rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
-       O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x)));
+       O nil l I Logic.eq_refl x Logic.eq_refl);
     rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
-       O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y)))
+       O nil l I Logic.eq_refl y Logic.eq_refl)
  end.
 trivial.
 Qed.
@@ -1352,15 +1339,15 @@ rewrite <-(
   let x := PEmul (num (Fnorm fe1))
                      (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
 ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe (refl_equal (Nmk_monpol_list lpe))
-        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+        Hlpe Logic.eq_refl
+        x Logic.eq_refl) in Hcrossprod.
 rewrite <-(
   let x := (PEmul (num (Fnorm fe2))
                      (rsplit_left
                         (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
     ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe (refl_equal (Nmk_monpol_list lpe))
-        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+        Hlpe Logic.eq_refl
+        x Logic.eq_refl) in Hcrossprod.
 simpl in Hcrossprod.
 rewrite Hcrossprod in |- *.
 reflexivity.
@@ -1392,15 +1379,15 @@ rewrite <-(
   let x := PEmul (num (Fnorm fe1))
                      (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
 ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe (refl_equal (Nmk_monpol_list lpe))
-        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+        Hlpe Logic.eq_refl
+        x Logic.eq_refl) in Hcrossprod.
 rewrite <-(
   let x := (PEmul (num (Fnorm fe2))
                      (rsplit_left
                         (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
     ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe (refl_equal (Nmk_monpol_list lpe))
-        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+        Hlpe Logic.eq_refl
+        x Logic.eq_refl) in Hcrossprod.
 simpl in Hcrossprod.
 rewrite Hcrossprod in |- *.
 reflexivity.
@@ -1756,7 +1743,7 @@ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
 Lemma add_inj_r : forall p x y,
    gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
 intros p x y.
-elim p using Pind; simpl in |- *; intros.
+elim p using Pos.peano_ind; simpl; intros.
  apply S_inj; trivial.
  apply H.
    apply S_inj.
@@ -1775,18 +1762,16 @@ case (Pos.compare_spec x y).
  intros.
    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.
-   now apply Pos.lt_gt.
+   symmetry.
+   rewrite (ARadd_0_r Rsth ARth).
+   rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth).
+   now rewrite Pos.add_comm, Pos.sub_add.
  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.
+   rewrite (ARadd_0_r Rsth ARth).
+   rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth).
+   now rewrite Pos.add_comm, Pos.sub_add.
 Qed.
 
 
@@ -1897,7 +1882,7 @@ Lemma gen_phiZ_complete : forall x y,
 intros.
  replace y with x.
  unfold Zeq_bool in |- *.
-   rewrite Zcompare_refl in |- *; trivial.
+   rewrite Z.compare_refl in |- *; trivial.
  apply gen_phiZ_inj; trivial.
 Qed.
 
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 763dbe7b9..bc0f888ce 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -27,14 +27,14 @@ Definition NotConstant := false.
 Lemma Zsth : Setoid_Theory Z (@eq Z).
 Proof (Eqsth Z).
 
-Lemma Zeqe : ring_eq_ext Zplus Zmult Zopp (@eq Z).
-Proof (Eq_ext Zplus Zmult Zopp).
+Lemma Zeqe : ring_eq_ext Z.add Z.mul Z.opp (@eq Z).
+Proof (Eq_ext Z.add Z.mul Z.opp).
 
-Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z).
+Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
 Proof.
- constructor. exact Zplus_0_l. exact Zplus_comm. exact Zplus_assoc.
- exact Zmult_1_l. exact Zmult_comm. exact Zmult_assoc.
- exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
+ constructor. exact Z.add_0_l. exact Z.add_comm. exact Z.add_assoc.
+ exact Z.mul_1_l. exact Z.mul_comm. exact Z.mul_assoc.
+ exact Z.mul_add_distr_r. trivial. exact Z.sub_diag.
 Qed.
 
 (** Two generic morphisms from Z to (abrbitrary) rings, *)
@@ -92,12 +92,12 @@ Section ZMORPHISM.
   | _ => None
   end.
 
- Lemma get_signZ_th : sign_theory Zopp Zeq_bool get_signZ.
+ Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ.
  Proof.
   constructor.
   destruct c;intros;try discriminate.
   injection H;clear H;intros H1;subst c'.
-  simpl. unfold Zeq_bool. rewrite Zcompare_refl. trivial.
+  simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
  Qed.
 
 
@@ -116,7 +116,7 @@ Section ZMORPHISM.
  Qed.
 
  Lemma ARgen_phiPOS_Psucc : forall x,
-   gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
+   gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
  Proof.
   induction x;simpl;norm.
   rewrite IHx;norm.
@@ -127,7 +127,7 @@ Section ZMORPHISM.
    gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
  Proof.
   induction x;destruct y;simpl;norm.
-  rewrite Pplus_carry_spec.
+  rewrite Pos.add_carry_spec.
   rewrite ARgen_phiPOS_Psucc.
   rewrite IHx;norm.
   add_push (gen_phiPOS1 y);add_push 1;rrefl.
@@ -208,10 +208,10 @@ Section ZMORPHISM.
 (*proof that [.] satisfies morphism specifications*)
  Lemma gen_phiZ_morph :
   ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH)
-   Zplus Zmult Zminus Zopp Zeq_bool gen_phiZ.
+   Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
  Proof.
   assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH)
-                  Zplus Zmult Zeq_bool gen_phiZ).
+                  Z.add Z.mul Zeq_bool gen_phiZ).
    apply mkRmorph;simpl;try rrefl.
    apply gen_phiZ_add.  apply gen_phiZ_mul. apply gen_Zeqb_ok.
   apply  (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
@@ -741,10 +741,10 @@ Ltac gen_ring_sign morph sspec :=
 Ltac default_div_spec set reqe arth morph :=
  match type of morph with
  | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               Z ?c0 ?c1 Zplus Zmult ?csub ?copp ?ceq_b ?phi =>
+               Z ?c0 ?c1 Z.add Z.mul ?csub ?copp ?ceq_b ?phi =>
       constr:(mkhypo (Ztriv_div_th set phi))
  | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               N ?c0 ?c1 Nplus Nmult ?csub ?copp ?ceq_b ?phi =>
+               N ?c0 ?c1 N.add N.mul ?csub ?copp ?ceq_b ?phi =>
       constr:(mkhypo (Ntriv_div_th set phi))
  | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
                ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
@@ -836,7 +836,7 @@ Ltac isPcst t :=
   | xO ?p => isPcst p
   | xH => constr:true
   (* nat -> positive *)
-  | P_of_succ_nat ?n => isnatcst n
+  | Pos.of_succ_nat ?n => isnatcst n
   | _ => constr:false
   end.
 
@@ -853,9 +853,9 @@ Ltac isZcst t :=
   | Zpos ?p => isPcst p
   | Zneg ?p => isPcst p
   (* injection nat -> Z *)
-  | Z_of_nat ?n => isnatcst n
+  | Z.of_nat ?n => isnatcst n
   (* injection N -> Z *)
-  | Z_of_N ?n => isNcst n
+  | Z.of_N ?n => isNcst n
   (* *)
   | _ => constr:false
   end.
diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v
index 5a224e38e..0c16fe1a3 100644
--- a/plugins/setoid_ring/Integral_domain.v
+++ b/plugins/setoid_ring/Integral_domain.v
@@ -19,7 +19,7 @@ rewrite H0. rewrite <- H. cring.
 Qed.
 
 
-Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n).
+Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N.of_nat n).
 
 Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0.
 induction n. unfold pow; simpl. intros. absurd (1 == 0). 
@@ -29,9 +29,8 @@ intros.
 case (integral_domain_product p (pow p n) H). trivial. trivial. 
 unfold pow; simpl. 
 clear IHn. induction n; simpl; try cring. 
- rewrite Ring_theory.pow_pos_Psucc. cring. apply ring_setoid.
+ rewrite Ring_theory.pow_pos_succ. cring. apply ring_setoid.
 apply ring_mult_comp.
-apply cring_mul_comm.
 apply ring_mul_assoc.
 Qed.
 
diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v
index 9a30fa47e..c093716b3 100644
--- a/plugins/setoid_ring/Ncring.v
+++ b/plugins/setoid_ring/Ncring.v
@@ -106,9 +106,10 @@ Context {R:Type}`{Rr:Ring R}.
 
 (* Powers *)
 
- Lemma pow_pos_comm : forall  x j,  x * pow_pos x j == pow_pos x j * x.
+Lemma pow_pos_comm : forall  x j,  x * pow_pos x j == pow_pos x j * x.
+Proof.
 induction j; simpl. rewrite <- ring_mul_assoc.
-rewrite <- ring_mul_assoc. 
+rewrite <- ring_mul_assoc.
 rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
 rewrite <- IHj. rewrite <- ring_mul_assoc. reflexivity.
 rewrite <- ring_mul_assoc. rewrite <- IHj.
@@ -116,10 +117,10 @@ rewrite ring_mul_assoc. rewrite IHj.
 rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity.
 Qed.
 
- Lemma pow_pos_Psucc : forall  x j, pow_pos x (Psucc j) == x * pow_pos x j.
- Proof.
-  induction j; simpl. 
-  rewrite IHj. 
+Lemma pow_pos_succ : forall  x j, pow_pos x (Pos.succ j) == x * pow_pos x j.
+Proof.
+induction j; simpl.
+  rewrite IHj.
 rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
 rewrite (ring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
   rewrite <- pow_pos_comm.
@@ -127,20 +128,20 @@ rewrite <- ring_mul_assoc. reflexivity.
 reflexivity. reflexivity.
 Qed.
 
- Lemma pow_pos_Pplus : forall  x i j,
-   pow_pos x (i + j) == pow_pos x i * pow_pos x j.
- Proof.
+Lemma pow_pos_add : forall  x i j,
+  pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+Proof.
   intro x;induction i;intros.
-  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  rewrite Pos.xI_succ_xO;rewrite <- Pos.add_1_r.
+  rewrite <- Pos.add_diag;repeat rewrite <- Pos.add_assoc.
   repeat rewrite IHi.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
-  rewrite pow_pos_Psucc.
+  rewrite Pos.add_comm;rewrite Pos.add_1_r;
+  rewrite pow_pos_succ.
   simpl;repeat rewrite ring_mul_assoc. reflexivity.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  rewrite <- Pos.add_diag;repeat rewrite <- Pos.add_assoc.
   repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc.
-   simpl. reflexivity. 
+  rewrite Pos.add_comm;rewrite Pos.add_1_r;rewrite pow_pos_succ.
+   simpl. reflexivity.
  Qed.
 
  Definition id_phi_N (x:N) : N := x.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 3c79f7d9b..90fd82054 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -27,20 +27,17 @@ Definition NotConstant := false.
 
 (** Z is a ring and a setoid*)
 
-Lemma Zsth : Setoid_Theory Z (@eq Z).
-constructor;red;intros;subst;trivial.
-Qed.
+Lemma Zsth : Equivalence (@eq Z).
+Proof. exact Z.eq_equiv. Qed.
 
-Instance Zops:@Ring_ops Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z).
+Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z).
 
 Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops).
-constructor;
-try (try apply Zsth;
-   try (unfold respectful, Proper; unfold equality; unfold eq_notation in *;
-  intros; try rewrite H; try rewrite H0; reflexivity)).
- exact Zplus_comm. exact Zplus_assoc.
- exact Zmult_1_l.  exact Zmult_1_r. exact Zmult_assoc.
- exact Zmult_plus_distr_l.  intros; apply Zmult_plus_distr_r.  exact Zminus_diag.
+Proof.
+constructor; try apply Zsth; try solve_proper.
+ exact Z.add_comm. exact Z.add_assoc.
+ exact Z.mul_1_l.  exact Z.mul_1_r. exact Z.mul_assoc.
+ exact Z.mul_add_distr_r.  intros; apply Z.mul_add_distr_l.  exact Z.sub_diag.
 Defined.
 
 (*Instance ZEquality: @Equality Z:= (@eq Z).*)
@@ -102,7 +99,7 @@ Ltac rsimpl := simpl.
  Qed.
 
  Lemma ARgen_phiPOS_Psucc : forall x,
-   gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
+   gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
  Proof.
   induction x;rsimpl;norm.
  rewrite IHx. gen_rewrite. add_push 1. reflexivity.
@@ -112,7 +109,7 @@ Ltac rsimpl := simpl.
    gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
  Proof.
   induction x;destruct y;simpl;norm.
-  rewrite Pplus_carry_spec.
+  rewrite Pos.add_carry_spec.
   rewrite ARgen_phiPOS_Psucc.
   rewrite IHx;norm.
   add_push (gen_phiPOS1 y);add_push 1;reflexivity.
@@ -152,20 +149,13 @@ Ltac rsimpl := simpl.
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
-  rewrite Z.pos_sub_spec.
-  assert (HH0 := Pminus_mask_Gt x y). unfold Pos.gt in HH0.
-  assert (HH1 := Pminus_mask_Gt y x). unfold Pos.gt in HH1.
-  rewrite Pos.compare_antisym in HH1.
-  destruct (Pos.compare_spec x y) as [HH|HH|HH].
-  subst. rewrite ring_opp_def;reflexivity.
-  destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial.
-  unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
-  rewrite ARgen_phiPOS_add;simpl;norm.
-  rewrite ring_opp_def;norm.
-  destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial.
-  unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
-  rewrite ARgen_phiPOS_add;simpl;norm.
-  add_push (gen_phiPOS1 h). rewrite ring_opp_def ; norm.
+  generalize (Z.pos_sub_discr x y).
+  destruct (Z.pos_sub x y) as [|p|p]; intros; subst.
+  - now rewrite ring_opp_def.
+  - rewrite ARgen_phiPOS_add;simpl;norm.
+    add_push (gen_phiPOS1 p). rewrite ring_opp_def;norm.
+  - rewrite ARgen_phiPOS_add;simpl;norm.
+    rewrite ring_opp_def;norm.
  Qed.
 
  Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
@@ -206,16 +196,14 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x].
 Global Instance gen_phiZ_morph :
 (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
  apply Build_Ring_morphism; simpl;try reflexivity.
-   apply gen_phiZ_add. intros. rewrite ring_sub_def. 
-replace (Zminus x y) with (x + (-y))%Z. rewrite gen_phiZ_add. 
-rewrite gen_phiZ_opp.  rewrite ring_sub_def. reflexivity.
+   apply gen_phiZ_add. intros. rewrite ring_sub_def.
+replace (x-y)%Z with (x + (-y))%Z.
+now rewrite gen_phiZ_add, gen_phiZ_opp, ring_sub_def.
 reflexivity.
- apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. 
+ apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext.
  Defined.
 
 End ZMORPHISM.
 
 Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication  :=
   {multiplication x y := (gen_phiZ x) * y}.
-
-
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 17dd2daa3..3c2900c39 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -52,7 +52,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
@@ -67,7 +67,7 @@ Instance equalityb_pol : Equalityb Pol :=
   match P with
   | Pc c => if c =? 0 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
@@ -109,13 +109,13 @@ 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' *)
         Lt => mkPX P' i' n' (PaddX i n Q')
       | (* i = i' *)
-        Eq => match ZPminus n n' with
+        Eq => match Z.pos_sub n n' with
               | (* n > n' *) 
                 Zpos k => mkPX (PaddX i k P') i' n' Q'
               | (* n = n' *)
@@ -178,61 +178,25 @@ Definition Psub(P P':Pol):= P ++ (--P').
 
  Reserved Notation "P @ l " (at level 10, no associativity).
  Notation "P @ l " := (Pphi l P).
+
  (** Proofs *)
- Lemma ZPminus_spec : forall x y,
-  match ZPminus x y with
-  | Z0 => x = y
-  | Zpos k => x = (y + k)%positive
-  | Zneg k => y = (x + k)%positive
+
+ Ltac destr_pos_sub H :=
+  match goal with |- context [Z.pos_sub ?x ?y] =>
+   assert (H := Z.pos_sub_discr x y); destruct (Z.pos_sub x y)
   end.
- Proof.
-  induction x;destruct y.
-  replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
-  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;
-rewrite Hh;trivial.
-  replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));
-trivial.
-  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;
-rewrite Hh;trivial.
-  apply Pplus_xI_double_minus_one.
-  simpl;trivial.
-  replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));
-trivial.
-  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;
-rewrite Hh;trivial.
-  apply Pplus_xI_double_minus_one.
-  replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
-  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite Hh;
-trivial.
-  replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
-  rewrite <- Pplus_one_succ_l.
-  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
-  replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
-  replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
-  rewrite <- Pplus_one_succ_l.
-  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
-  simpl;trivial.
- Qed.
 
  Lemma Peq_ok : forall 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 (H1h := IHP1 P'1);assert (H2h := IHP2 P'2).
-   simpl in H1h. destruct (Peq P2 P'1). simpl in H2h; 
-destruct (Peq P3 P'2).
-  rewrite (H1h);trivial . rewrite (H2h);trivial. 
-assert (H3h := Pcompare_Eq_eq p p1);
- destruct (Pos.compare_cont p p1 Eq);
-assert (H4h := Pcompare_Eq_eq p0 p2);
-destruct (Pos.compare_cont p0 p2 Eq); try (discriminate H).
- rewrite H3h;trivial. rewrite H4h;trivial. reflexivity.
- destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq);
- try (discriminate H).
- destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq);
- try (discriminate H). 
+ induction P;destruct P';simpl;intros ;try easy.
+ - now apply ring_morphism_eq, Ceqb_eq.
+ - specialize (IHP1 P'1). specialize (IHP2 P'2).
+   simpl in IHP1, IHP2.
+   destruct (Pos.compare_spec p p1); try discriminate;
+   destruct (Pos.compare_spec p0 p2); try discriminate.
+   destruct (Peq P2 P'1); try discriminate.
+   subst; now rewrite IHP1, IHP2.
  Qed.
 
  Lemma Pphi0 : forall l, P0@l == 0.
@@ -255,12 +219,12 @@ destruct (Pos.compare_cont p0 p2 Eq); try (discriminate H).
 simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
 intros.
   rewrite Hh. rewrite ring_morphism0.
-  rsimpl. apply Ceqb_eq. trivial. assert (Hh1 := Pcompare_Eq_eq i p);
-destruct (Pos.compare_cont i p Eq).
+  rsimpl. apply Ceqb_eq. trivial.
+  destruct (Pos.compare_spec i p).
   assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. 
   rewrite Hh. 
-  rewrite Pphi0. rsimpl. rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl.
-rewrite Hh1;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity.
+  rewrite Pphi0. rsimpl. rewrite Pos.add_comm. rewrite pow_pos_add;rsimpl.
+  subst;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity.
  simpl. reflexivity.
  Qed.
 
@@ -331,13 +295,13 @@ 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' *)
         Lt => mkPX P' i' n' (PaddX Padd P i n Q')
       | (* i = i' *)
-        Eq => match ZPminus n n' with
+        Eq => match Z.pos_sub n n' with
               | (* n > n' *) 
                 Zpos k => mkPX (PaddX Padd P i k P') i' n' Q'
               | (* n = n' *)
@@ -359,17 +323,17 @@ Lemma PaddX_ok2 : forall P2,
 induction P2;simpl;intros. split. intros. apply PaddCl_ok.
  induction P.  unfold PaddX. intros. rewrite mkPX_ok.
  simpl. rsimpl.
-intros. simpl. assert (Hh := Pcompare_Eq_eq k p);
- destruct (Pos.compare_cont k p Eq).
- assert (H1h := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2.
+intros. simpl.
+ destruct (Pos.compare_spec k p) as [Hh|Hh|Hh].
+ destr_pos_sub H1h. Esimpl2.
 rewrite Hh; trivial. rewrite H1h. reflexivity.
 simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2.
- rewrite Pplus_comm in H1h.
+ rewrite Pos.add_comm in H1h.
 rewrite H1h. 
-rewrite pow_pos_Pplus.  Esimpl2.
+rewrite pow_pos_add.  Esimpl2.
 rewrite Hh; trivial. reflexivity.
-rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1h.
-rewrite H1h.  Esimpl2. rewrite pow_pos_Pplus. Esimpl2.
+rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pos.add_comm in H1h.
+rewrite H1h.  Esimpl2. rewrite pow_pos_add. Esimpl2.
 rewrite Hh; trivial. reflexivity.
 rewrite mkPX_ok. rewrite IHP2. Esimpl2.
 rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) 
@@ -382,19 +346,18 @@ split. intros. rewrite H0. rewrite H1.
 Esimpl2.
 induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity.
 intros. rewrite PaddXPX. 
-assert (H3h := Pcompare_Eq_eq k p1);
- destruct (Pos.compare_cont k p1 Eq).
-assert (H4h := ZPminus_spec n p2);destruct (ZPminus n p2). 
+destruct (Pos.compare_spec k p1) as [H3h|H3h|H3h].
+destr_pos_sub H4h.
 rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2.
 rewrite H4h. rewrite H3h;trivial. reflexivity.
 rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial.
-rewrite Pplus_comm in H4h.
-rewrite H4h. rewrite pow_pos_Pplus. Esimpl2.
+rewrite Pos.add_comm in H4h.
+rewrite H4h. rewrite pow_pos_add. Esimpl2.
 rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. 
 rewrite mkPX_ok.
  Esimpl2. rewrite H3h;trivial.
- rewrite Pplus_comm in H4h.
-rewrite H4h. rewrite pow_pos_Pplus. Esimpl2.
+ rewrite Pos.add_comm in H4h.
+rewrite H4h. rewrite pow_pos_add. Esimpl2.
 rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2.
 gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity.
 rewrite mkPX_ok. simpl. reflexivity.
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
index d7cee83a5..6da54576d 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -104,7 +104,7 @@ Instance  reify_pow (R:Type) `{Ring R}
 Instance  reify_var (R:Type) t lvar i 
  `{nth R t lvar i}
  `{Rr: Ring (T:=R)}
- : reify (Rr:= Rr) (PEX Z (P_of_succ_nat i))lvar t 
+ : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t
  | 100.
 
 Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) 
@@ -202,7 +202,7 @@ Ltac ring_simplify_aux lterm fv lexpr hyp :=
     match lexpr with
       | ?e::?le => (* e:PExpr Z est la réification de t0:R *)
         let t := constr:(@Ncring_polynom.norm_subst
-          Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z) Zops Zeq_bool e) in
+          Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z) Zops Zeq_bool e) in
         (* t:Pol Z *)
         let te := 
           constr:(@Ncring_polynom.Pphi Z 
@@ -212,13 +212,13 @@ Ltac ring_simplify_aux lterm fv lexpr hyp :=
         let t':= fresh "t" in
         pose (t' := nft);
         assert (eq1 : t = t');
-        [vm_cast_no_check (refl_equal t')|
+        [vm_cast_no_check (eq_refl t')|
         let eq2 := fresh "ring" in
         assert (eq2:(@Ncring_polynom.PEeval Z
           _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ N (fun n:N => n) 
           (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
         [apply (@Ncring_polynom.norm_subst_ok
-          Z _ 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z)
+          Z _ 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z)
           _ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _
           (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok);
            apply mkpow_th; reflexivity
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 56473adb9..14c4270f9 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -111,19 +111,19 @@ Proof.
   intros n0 H' m; rewrite H'; auto with real.
 Qed.
 
-Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R))  nat_of_N pow.
+Lemma R_power_theory : power_theory 1%R Rmult (@eq R) N.to_nat pow.
 Proof.
  constructor. destruct n. reflexivity.
- simpl. induction p;simpl.
- rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity.
- unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial.
- rewrite Rmult_comm;apply Rmult_1_l.
+ simpl. induction p.
+ - rewrite Pos2Nat.inj_xI. simpl. now rewrite plus_0_r, Rdef_pow_add, IHp.
+ - rewrite Pos2Nat.inj_xO. simpl. now rewrite plus_0_r, Rdef_pow_add, IHp.
+ - simpl. rewrite Rmult_comm;apply Rmult_1_l.
 Qed.
 
 Ltac Rpow_tac t :=
   match isnatcst t with
   | false => constr:(InitialRing.NotConstant)
-  | _ => constr:(N_of_nat t)
+  | _ => constr:(N.of_nat t)
   end.
 
 Add Field RField : Rfield
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index b722a31b6..4b4332e17 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -7,14 +7,10 @@
 (************************************************************************)
 
 Set Implicit Arguments.
-Require Import Setoid.
-Require Import BinList.
-Require Import BinPos.
-Require Import BinNat.
-Require Import BinInt.
+Require Import Setoid BinList BinPos BinNat BinInt.
 Require Export Ring_theory.
 
-Open Local Scope positive_scope.
+Local Open Scope positive_scope.
 Import RingSyntax.
 
 Section MakeRingPol.
@@ -25,7 +21,7 @@ Section MakeRingPol.
  Variable req : R -> R -> Prop.
 
  (* Ring properties *)
- Variable Rsth : Setoid_Theory R req.
+ Variable Rsth : Equivalence req.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
  Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
 
@@ -60,8 +56,6 @@ Section MakeRingPol.
  Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
 
  (* Useful tactics *)
-  Add Setoid R req Rsth as R_set1.
- Ltac rrefl := gen_reflexivity Rsth.
   Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
   Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
@@ -128,7 +122,7 @@ Section MakeRingPol.
  Definition mkPinj_pred j P:=
   match j with
   | xH => P
-  | xO j => Pinj (Pdouble_minus_one j) P
+  | xO j => Pinj (Pos.pred_double j) P
   | xI j => Pinj (xO j) P
   end.
 
@@ -179,7 +173,7 @@ Section MakeRingPol.
    match P with
    | Pc c => mkPinj j (PaddC Q c)
    | Pinj j' Q' =>
-     match ZPminus j' j with
+     match Z.pos_sub j' j with
      | Zpos k =>  mkPinj j (Pop (Pinj k Q') Q)
      | Z0 => mkPinj j (Pop Q' Q)
      | Zneg k => mkPinj j' (PaddI k Q')
@@ -187,7 +181,7 @@ Section MakeRingPol.
    | PX P i Q' =>
      match j with
      | xH => PX P i (Pop Q' Q)
-     | xO j => PX P i (PaddI (Pdouble_minus_one j) Q')
+     | xO j => PX P i (PaddI (Pos.pred_double j) Q')
      | xI j => PX P i (PaddI (xO j) Q')
      end
    end.
@@ -196,7 +190,7 @@ Section MakeRingPol.
    match P with
    | Pc c => mkPinj j (PaddC (--Q) c)
    | Pinj j' Q' =>
-     match ZPminus j' j with
+     match Z.pos_sub j' j with
      | Zpos k =>  mkPinj j (Pop (Pinj k Q') Q)
      | Z0 => mkPinj j (Pop Q' Q)
      | Zneg k => mkPinj j' (PsubI k Q')
@@ -204,7 +198,7 @@ Section MakeRingPol.
    | PX P i Q' =>
      match j with
      | xH => PX P i (Pop Q' Q)
-     | xO j => PX P i (PsubI (Pdouble_minus_one j) Q')
+     | xO j => PX P i (PsubI (Pos.pred_double j) Q')
      | xI j => PX P i (PsubI (xO j) Q')
      end
    end.
@@ -217,11 +211,11 @@ Section MakeRingPol.
   | Pinj j Q' =>
     match j with
     | xH =>  PX P' i' Q'
-    | xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q')
+    | xO j => PX P' i' (Pinj (Pos.pred_double j) Q')
     | xI j => PX P' i' (Pinj (xO j) Q')
     end
   | PX P i Q' =>
-    match ZPminus i i' with
+    match Z.pos_sub i i' with
     | Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
     | Z0 => mkPX (Pop P P') i Q'
     | Zneg k => mkPX (PaddX k P) i Q'
@@ -234,11 +228,11 @@ Section MakeRingPol.
   | Pinj j Q' =>
     match j with
     | xH =>  PX (--P') i' Q'
-    | xO j => PX (--P') i' (Pinj (Pdouble_minus_one j) Q')
+    | xO j => PX (--P') i' (Pinj (Pos.pred_double j) Q')
     | xI j => PX (--P') i' (Pinj (xO j) Q')
     end
   | PX P i Q' =>
-    match ZPminus i i' with
+    match Z.pos_sub i i' with
     | Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
     | Z0 => mkPX (Pop P P') i Q'
     | Zneg k => mkPX (PsubX k P) i Q'
@@ -258,11 +252,11 @@ Section MakeRingPol.
     | Pinj j Q =>
       match j with
       | xH => PX P' i' (Padd Q Q')
-      | xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q')
+      | xO j => PX P' i' (Padd (Pinj (Pos.pred_double j) Q) Q')
       | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q')
       end
     | PX P i Q =>
-      match ZPminus i i' with
+      match Z.pos_sub i i' with
       | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q')
       | Z0 => mkPX (Padd P P') i (Padd Q Q')
       | Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q')
@@ -281,11 +275,11 @@ Section MakeRingPol.
     | Pinj j Q =>
       match j with
       | xH => PX (--P') i' (Psub Q Q')
-      | xO j => PX (--P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q')
+      | xO j => PX (--P') i' (Psub (Pinj (Pos.pred_double j) Q) Q')
       | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q')
       end
     | PX P i Q =>
-      match ZPminus i i' with
+      match Z.pos_sub i i' with
       | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q')
       | Z0 => mkPX (Psub P P') i (Psub Q Q')
       | Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q')
@@ -314,7 +308,7 @@ Section MakeRingPol.
    match P with
    | Pc c => mkPinj j (PmulC Q c)
    | Pinj j' Q' =>
-     match ZPminus j' j with
+     match Z.pos_sub j' j with
      | Zpos k => mkPinj j (Pmul (Pinj k Q') Q)
      | Z0 => mkPinj j (Pmul Q' Q)
      | Zneg k => mkPinj j' (PmulI k Q')
@@ -322,13 +316,12 @@ Section MakeRingPol.
    | PX P' i' Q' =>
      match j with
      | xH => mkPX (PmulI xH P') i' (Pmul Q' Q)
-     | xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q')
+     | xO j' => mkPX (PmulI j P') i' (PmulI (Pos.pred_double j') Q')
      | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q')
      end
    end.
 
  End PmulI.
-(* A symmetric version of the multiplication *)
 
  Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
    match P'' with
@@ -341,7 +334,7 @@ Section MakeRingPol.
        let QQ' :=
          match j with
          | xH => Pmul Q Q'
-         | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q'
+         | xO j => Pmul (Pinj (Pos.pred_double j) Q) Q'
          | xI j => Pmul (Pinj (xO j) Q) Q'
          end in
        mkPX (Pmul P P') i' QQ'
@@ -354,24 +347,6 @@ Section MakeRingPol.
      end
   end.
 
-(* Non symmetric *)
-(*
- Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol :=
-  match P' with
-  | Pc c' => PmulC P c'
-  | Pinj j' Q' => PmulI Pmul_aux Q' j' P
-  | PX P' i' Q' =>
-     (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P)
-  end.
-
- Definition Pmul P P' :=
-  match P with
-  | Pc c => PmulC P' c
-  | Pinj j Q => PmulI Pmul_aux Q j P'
-  | PX P i Q =>
-    (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P')
-  end.
-*)
  Notation "P ** P'" := (Pmul P P').
 
  Fixpoint Psquare (P:Pol) : Pol :=
@@ -406,7 +381,7 @@ Section MakeRingPol.
    match M with mon0 => mon0 | _ => zmon j M end.
 
  Definition zmon_pred j M :=
-   match j with xH => M | _ => mkZmon (Ppred j) M end.
+   match j with xH => M | _ => mkZmon (Pos.pred j) M end.
 
  Definition mkVmon i M :=
    match M with
@@ -517,51 +492,26 @@ Section MakeRingPol.
 
  Reserved Notation "P @ l " (at level 10, no associativity).
  Notation "P @ l " := (Pphi l P).
+
  (** Proofs *)
- Lemma ZPminus_spec : forall x y,
-  match ZPminus x y with
-  | Z0 => x = y
-  | Zpos k => x = (y + k)%positive
-  | Zneg k => y = (x + k)%positive
+
+ Ltac destr_pos_sub H :=
+  match goal with |- context [Z.pos_sub ?x ?y] =>
+   assert (H := Z.pos_sub_discr x y); destruct (Z.pos_sub x y)
   end.
- Proof.
-  induction x;destruct y.
-  replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
-  replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial.
-  apply Pplus_xI_double_minus_one.
-  simpl;trivial.
-  replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial.
-  apply Pplus_xI_double_minus_one.
-  replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
-  replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
-  rewrite <- Pplus_one_succ_l.
-  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
-  replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
-  replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
-  rewrite <- Pplus_one_succ_l.
-  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
-  simpl;trivial.
- Qed.
 
  Lemma Peq_ok : forall P P',
     (P ?== P') = true -> forall l, P@l == P'@ l.
  Proof.
-  induction P;destruct P';simpl;intros;try discriminate;trivial.
-  apply (morph_eq CRmorph);trivial.
-  assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
-   try discriminate H.
-  rewrite (IHP P' H); rewrite H1;trivial;rrefl.
-  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);
-   destruct (P2 ?== P'1);[destruct (P3 ?== P'2); [idtac|discriminate H]
-                         |discriminate H].
-  rewrite (H1 H);rewrite (H2 H);rrefl.
+  induction P;destruct P';simpl; intros H l; try easy.
+  - now apply (morph_eq CRmorph).
+  - destruct (Pos.compare_spec p p0); [ subst | easy | easy ].
+    now rewrite IHP.
+  - specialize (IHP1 P'1); specialize (IHP2 P'2).
+    destruct (Pos.compare_spec p p0); [ subst | easy | easy ].
+    destruct (P2 ?== P'1); [|easy].
+    rewrite H in *.
+    now rewrite IHP1, IHP2.
  Qed.
 
  Lemma Pphi0 : forall l, P0@l == 0.
@@ -577,23 +527,23 @@ Section MakeRingPol.
  Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).
  Proof.
   intros j l p;destruct p;simpl;rsimpl.
-  rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl.
+  rewrite <-jump_add;rewrite Pos.add_comm;reflexivity.
  Qed.
 
- Let pow_pos_Pplus :=
-    pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
+ Let pow_pos_add :=
+    pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc).
 
  Lemma mkPX_ok : forall l P i Q,
   (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l).
  Proof.
   intros l P i Q;unfold mkPX.
-  destruct P;try (simpl;rrefl).
-  assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try rrefl.
-  rewrite (H (refl_equal true));rewrite (morph0 CRmorph).
-  rewrite mkPinj_ok;rsimpl;simpl;rrefl.
-  assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl.
-  rewrite (H (refl_equal true));trivial.
-  rewrite Pphi0.  rewrite pow_pos_Pplus;rsimpl.
+  destruct P;try (simpl;reflexivity).
+  assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try reflexivity.
+  rewrite (H (eq_refl true));rewrite (morph0 CRmorph).
+  rewrite mkPinj_ok;rsimpl;simpl;reflexivity.
+  assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try reflexivity.
+  rewrite (H (eq_refl true));trivial.
+  rewrite Pphi0.  rewrite pow_pos_add;rsimpl.
  Qed.
 
  Ltac Esimpl :=
@@ -636,16 +586,16 @@ Section MakeRingPol.
  Proof.
   induction P;simpl;intros;Esimpl;trivial.
   rewrite IHP1;rewrite IHP2;rsimpl.
-  mul_push ([c]);rrefl.
+  mul_push ([c]);reflexivity.
  Qed.
 
  Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
  Proof.
   intros c P l; unfold PmulC.
   assert (H:= morph_eq CRmorph c cO);destruct (c ?=! cO).
-  rewrite (H (refl_equal true));Esimpl.
+  rewrite (H (eq_refl true));Esimpl.
   assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
-  rewrite (H1 (refl_equal true));Esimpl.
+  rewrite (H1 (eq_refl true));Esimpl.
   apply PmulC_aux_ok.
  Qed.
 
@@ -673,51 +623,51 @@ Section MakeRingPol.
   generalize P p l;clear P p l.
   induction P;simpl;intros.
   Esimpl2;apply (ARadd_comm ARth).
-  assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
-  rewrite H;Esimpl. rewrite IHP';rrefl.
+  destr_pos_sub H.
+  rewrite H;Esimpl. rewrite IHP';reflexivity.
   rewrite H;Esimpl. rewrite IHP';Esimpl.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
+  rewrite <- jump_add;rewrite Pos.add_comm;reflexivity.
   rewrite H;Esimpl. rewrite IHP.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
+  rewrite <- jump_add;rewrite Pos.add_comm;reflexivity.
   destruct p0;simpl.
   rewrite IHP2;simpl;rsimpl.
   rewrite IHP2;simpl.
-  rewrite jump_Pdouble_minus_one;rsimpl.
+  rewrite jump_pred_double;rsimpl.
   rewrite IHP';rsimpl.
   destruct P;simpl.
-  Esimpl2;add_push [c];rrefl.
+  Esimpl2;add_push [c];reflexivity.
   destruct p0;simpl;Esimpl2.
   rewrite IHP'2;simpl.
-  rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
+  rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));reflexivity.
   rewrite IHP'2;simpl.
-  rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
-  rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl.
-  assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
+  rewrite jump_pred_double;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));reflexivity.
+  rewrite IHP'2;rsimpl. add_push (P @ (tail l));reflexivity.
+  destr_pos_sub H; Esimpl2.
   rewrite IHP'1;rewrite IHP'2;rsimpl.
-  add_push (P3 @ (tail l));rewrite H;rrefl.
+  add_push (P3 @ (tail l));rewrite H;reflexivity.
   rewrite IHP'1;rewrite IHP'2;simpl;Esimpl.
-  rewrite H;rewrite Pplus_comm.
-  rewrite pow_pos_Pplus;rsimpl.
-  add_push (P3 @ (tail l));rrefl.
+  rewrite H;rewrite Pos.add_comm.
+  rewrite pow_pos_add;rsimpl.
+  add_push (P3 @ (tail l));reflexivity.
   assert (forall P k l,
            (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k).
    induction P;simpl;intros;try apply (ARadd_comm ARth).
    destruct p2;simpl;try apply (ARadd_comm ARth).
-   rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth).
-    assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2.
-    rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl.
+   rewrite jump_pred_double;apply (ARadd_comm ARth).
+    destr_pos_sub H1; Esimpl2.
+    rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));reflexivity.
     rewrite IHP'1;simpl;Esimpl.
-    rewrite H1;rewrite Pplus_comm.
-    rewrite pow_pos_Pplus;simpl;Esimpl.
-    add_push (P5 @ (tail l0));rrefl.
-    rewrite IHP1;rewrite H1;rewrite Pplus_comm.
-    rewrite pow_pos_Pplus;simpl;rsimpl.
-    add_push (P5 @ (tail l0));rrefl.
+    rewrite H1;rewrite Pos.add_comm.
+    rewrite pow_pos_add;simpl;Esimpl.
+    add_push (P5 @ (tail l0));reflexivity.
+    rewrite IHP1;rewrite H1;rewrite Pos.add_comm.
+    rewrite pow_pos_add;simpl;rsimpl.
+    add_push (P5 @ (tail l0));reflexivity.
   rewrite H0;rsimpl.
   add_push (P3 @ (tail l)).
-  rewrite H;rewrite Pplus_comm.
-  rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl.
-  add_push (P3 @ (tail l));rrefl.
+  rewrite H;rewrite Pos.add_comm.
+  rewrite IHP'2;rewrite pow_pos_add;rsimpl.
+  add_push (P3 @ (tail l));reflexivity.
  Qed.
 
  Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
@@ -726,54 +676,53 @@ Section MakeRingPol.
   generalize P p l;clear P p l.
   induction P;simpl;intros.
   Esimpl2;apply (ARadd_comm ARth).
-  assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
+  destr_pos_sub H.
   rewrite H;Esimpl. rewrite IHP';rsimpl.
   rewrite H;Esimpl. rewrite IHP';Esimpl.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
+  rewrite <- jump_add;rewrite Pos.add_comm;reflexivity.
   rewrite H;Esimpl. rewrite IHP.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
+  rewrite <- jump_add;rewrite Pos.add_comm;reflexivity.
   destruct p0;simpl.
   rewrite IHP2;simpl;rsimpl.
   rewrite IHP2;simpl.
-  rewrite jump_Pdouble_minus_one;rsimpl.
+  rewrite jump_pred_double;rsimpl.
   rewrite IHP';rsimpl.
   destruct P;simpl.
-  repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl.
+  repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try reflexivity.
   destruct p0;simpl;Esimpl2.
   rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial.
-  add_push (P @ (jump p0 (jump p0 (tail l))));rrefl.
-  rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl.
-  add_push (- (P'1 @ l * pow_pos  rmul (hd 0 l) p));rrefl.
-  rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl.
-  assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
+  add_push (P @ (jump p0 (jump p0 (tail l))));reflexivity.
+  rewrite IHP'2;simpl;rewrite jump_pred_double;rsimpl.
+  add_push (- (P'1 @ l * pow_pos  rmul (hd 0 l) p));reflexivity.
+  rewrite IHP'2;rsimpl;add_push (P @ (tail l));reflexivity.
+  destr_pos_sub H; Esimpl2.
   rewrite IHP'1; rewrite IHP'2;rsimpl.
-  add_push (P3 @ (tail l));rewrite H;rrefl.
+  add_push (P3 @ (tail l));rewrite H;reflexivity.
    rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl.
-  rewrite H;rewrite Pplus_comm.
-  rewrite pow_pos_Pplus;rsimpl.
-  add_push (P3 @ (tail l));rrefl.
+  rewrite H;rewrite Pos.add_comm.
+  rewrite pow_pos_add;rsimpl.
+  add_push (P3 @ (tail l));reflexivity.
   assert (forall P k l,
            (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k).
    induction P;simpl;intros.
    rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial.
    destruct p2;simpl;rewrite Popp_ok;rsimpl.
    apply (ARadd_comm ARth);trivial.
-   rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth);trivial.
+   rewrite jump_pred_double;apply (ARadd_comm ARth);trivial.
    apply (ARadd_comm ARth);trivial.
-    assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl.
-    rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl.
-    rewrite IHP'1;rewrite H1;rewrite Pplus_comm.
-    rewrite pow_pos_Pplus;simpl;Esimpl.
-    add_push (P5 @ (tail l0));rrefl.
-    rewrite IHP1;rewrite H1;rewrite Pplus_comm.
-    rewrite pow_pos_Pplus;simpl;rsimpl.
-    add_push (P5 @ (tail l0));rrefl.
+    destr_pos_sub H1; Esimpl2; rsimpl.
+    rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;reflexivity.
+    rewrite IHP'1;rewrite H1;rewrite Pos.add_comm.
+    rewrite pow_pos_add;simpl;Esimpl.
+    add_push (P5 @ (tail l0));reflexivity.
+    rewrite IHP1;rewrite H1;rewrite Pos.add_comm.
+    rewrite pow_pos_add;simpl;rsimpl.
+    add_push (P5 @ (tail l0));reflexivity.
   rewrite H0;rsimpl.
   rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)).
-  rewrite H;rewrite Pplus_comm.
-  rewrite pow_pos_Pplus;rsimpl.
+  rewrite H;rewrite Pos.add_comm.
+  rewrite pow_pos_add;rsimpl.
  Qed.
-(* Proof for the symmetriv version *)
 
  Lemma PmulI_ok :
   forall P',
@@ -783,60 +732,23 @@ Section MakeRingPol.
  Proof.
   induction P;simpl;intros.
   Esimpl2;apply (ARmul_comm ARth).
-  assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
-  rewrite H1; rewrite H;rrefl.
+  destr_pos_sub H1; Esimpl2.
+  rewrite H1; rewrite H;reflexivity.
   rewrite H1; rewrite H.
-  rewrite Pplus_comm.
-  rewrite jump_Pplus;simpl;rrefl.
-  rewrite H1;rewrite Pplus_comm.
-  rewrite jump_Pplus;rewrite IHP;rrefl.
+  rewrite Pos.add_comm.
+  rewrite jump_add;simpl;reflexivity.
+  rewrite H1;rewrite Pos.add_comm.
+  rewrite jump_add;rewrite IHP;reflexivity.
   destruct p0;Esimpl2.
   rewrite IHP1;rewrite IHP2;simpl;rsimpl.
-  mul_push (pow_pos rmul (hd 0 l) p);rrefl.
+  mul_push (pow_pos rmul (hd 0 l) p);reflexivity.
   rewrite IHP1;rewrite IHP2;simpl;rsimpl.
-  mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
+  mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_pred_double;reflexivity.
   rewrite IHP1;simpl;rsimpl.
   mul_push (pow_pos rmul (hd 0 l) p).
-  rewrite H;rrefl.
+  rewrite H;reflexivity.
  Qed.
 
-(*
- Lemma PmulI_ok :
-  forall P',
-   (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) ->
-   forall (P : Pol) (p : positive) (l : list R),
-    (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l).
- Proof.
-  induction P;simpl;intros.
-  Esimpl2;apply (ARmul_comm ARth).
-  assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
-  rewrite H1; rewrite H;rrefl.
-  rewrite H1; rewrite H.
-  rewrite Pplus_comm.
-  rewrite jump_Pplus;simpl;rrefl.
-  rewrite H1;rewrite Pplus_comm.
-  rewrite jump_Pplus;rewrite IHP;rrefl.
-  destruct p0;Esimpl2.
-  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
-  mul_push (pow_pos rmul (hd 0 l) p);rrefl.
-  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
-  mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
-  rewrite IHP1;simpl;rsimpl.
-  mul_push (pow_pos rmul (hd 0 l) p).
-  rewrite H;rrefl.
- Qed.
-
- Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux P P')@l == P@l * P'@l.
- Proof.
-  induction P';simpl;intros.
-  Esimpl2;trivial.
-  apply PmulI_ok;trivial.
-  rewrite Padd_ok;Esimpl2.
-  rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl.
- Qed.
-*)
-
-(* Proof for the symmetric version *)
  Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
  Proof.
   intros P P';generalize P;clear P;induction P';simpl;intros.
@@ -846,11 +758,11 @@ Section MakeRingPol.
   Esimpl2. rewrite IHP'1;Esimpl2.
    assert (match p0 with
            | xI j => Pinj (xO j) P ** P'2
-           | xO j => Pinj (Pdouble_minus_one j) P ** P'2
+           | xO j => Pinj (Pos.pred_double j) P ** P'2
            | 1 => P ** P'2
            end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)).
    destruct p0;simpl;rewrite IHP'2;Esimpl.
-   rewrite jump_Pdouble_minus_one;Esimpl.
+   rewrite jump_pred_double;Esimpl.
    rewrite H;Esimpl.
    rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2.
    repeat (rewrite IHP'1 || rewrite IHP'2);simpl.
@@ -858,27 +770,13 @@ Section MakeRingPol.
    mul_push (P'1@l). simpl. mul_push (P'2 @ (tail l)). Esimpl.
  Qed.
 
-(*
-Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
- Proof.
-  destruct P;simpl;intros.
-  Esimpl2;apply (ARmul_comm ARth).
-  rewrite (PmulI_ok P (Pmul_aux_ok P)).
-  apply (ARmul_comm ARth).
-  rewrite Padd_ok; Esimpl2.
-  rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial.
-  rewrite Pmul_aux_ok;mul_push (P' @ l).
-  rewrite (ARmul_comm ARth (P' @ l));rrefl.
- Qed.
-*)
-
  Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
  Proof.
   induction P;simpl;intros;Esimpl2.
   apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2.
   rewrite IHP1;rewrite IHP2.
   mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l).
-  rrefl.
+  reflexivity.
  Qed.
 
 
@@ -892,14 +790,14 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
  Proof.
    destruct j; simpl;intros auto; rsimpl.
    rewrite mkZmon_ok;rsimpl.
-   rewrite mkZmon_ok;simpl. rewrite jump_Pdouble_minus_one; rsimpl.
+   rewrite mkZmon_ok;simpl. rewrite jump_pred_double; rsimpl.
  Qed.
 
  Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i.
  Proof.
   destruct M;simpl;intros;rsimpl.
    rewrite zmon_pred_ok;simpl;rsimpl.
-  rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl.
+  rewrite Pos.add_comm;rewrite pow_pos_add;rsimpl.
  Qed.
 
  Lemma Mcphi_ok: forall P c l,
@@ -930,9 +828,9 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
       P@l == Q@l + (phi c) * (Mphi l M) * (R@l).
  Proof.
  intros P; elim P; simpl; auto; clear P.
-   intros c (c1, M) l; case M; simpl; auto.
+ - intros c (c1, M) l; case M; simpl; auto.
    assert (H1:= morph_eq CRmorph c1 cI);destruct (c1 ?=! cI).
-   rewrite (H1 (refl_equal true));Esimpl.
+   rewrite (H1 (eq_refl true));Esimpl.
     try rewrite (morph0 CRmorph); rsimpl.
    generalize (div_th.(div_eucl_th) c c1); case (cdiv c c1).
    intros q r H; rewrite H; clear H H1.
@@ -940,39 +838,39 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    rewrite (ARadd_comm ARth); rsimpl.
    intros p m; Esimpl.
    intros p m; Esimpl.
-   intros i P Hrec (c,M) l; case M; simpl; clear M.
-     assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
-     rewrite (H1 (refl_equal true));Esimpl.
+ - intros i P Hrec (c,M) l; case M; simpl; clear M.
+   + assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
+     rewrite (H1 (eq_refl true));Esimpl.
      Esimpl.
-   generalize (Mcphi_ok P c (jump i l)); case CFactor.
-   intros R1 Q1 HH; rewrite HH; Esimpl.
-     intros j M.
-     case_eq (i ?= j); intros He; simpl.
-       rewrite (Pos.compare_eq _ _ He).
+     generalize (Mcphi_ok P c (jump i l)); case CFactor.
+     intros R1 Q1 HH; rewrite HH; Esimpl.
+   + intros j M.
+     case Pos.compare_spec; intros He; simpl.
+     * rewrite 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));
+     * generalize (Hrec (c, (zmon (j -i) M)) (jump i l));
        case (MFactor P c (zmon (j -i) M)); simpl.
        intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
-       rewrite  <- (Pplus_minus _ _ (ZC2 _ _ He)).
-       rewrite Pplus_comm; rewrite jump_Pplus; auto.
-       rewrite (morph0 CRmorph); rsimpl.
-       intros P2 m; rewrite (morph0 CRmorph); rsimpl.
-
-   intros P2 Hrec1 i Q2 Hrec2 (c, M) l; case M; simpl; auto.
-     assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
-     rewrite (H1 (refl_equal true));Esimpl.
+       rewrite  <- (Pos.sub_add _ _ He).
+       rewrite jump_add; auto.
+     * rewrite (morph0 CRmorph); rsimpl.
+   + intros P2 m; rewrite (morph0 CRmorph); rsimpl.
+
+ - intros P2 Hrec1 i Q2 Hrec2 (c, M) l; case M; simpl; auto.
+   + assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
+     rewrite (H1 (eq_refl true));Esimpl.
      Esimpl.
-    generalize (Mcphi_ok P2 c l); case CFactor.
-    intros S1 S2 HS.
-    generalize (Mcphi_ok Q2 c (tail l)); case CFactor.
-    intros S3 S4 HS1; Esimpl; rewrite HS; rewrite HS1.
-    rsimpl.
-    apply (Radd_ext Reqe); rsimpl.
-    repeat rewrite <- (ARadd_assoc ARth).
-    apply (Radd_ext Reqe); rsimpl.
-    rewrite (ARadd_comm ARth); rsimpl.
-   intros j M1.
+     generalize (Mcphi_ok P2 c l); case CFactor.
+     intros S1 S2 HS.
+     generalize (Mcphi_ok Q2 c (tail l)); case CFactor.
+     intros S3 S4 HS1; Esimpl; rewrite HS; rewrite HS1.
+     rsimpl.
+     apply (Radd_ext Reqe); rsimpl.
+     repeat rewrite <- (ARadd_assoc ARth).
+     apply (Radd_ext Reqe); rsimpl.
+     rewrite (ARadd_comm ARth); rsimpl.
+   + intros j M1.
      generalize (Hrec1 (c,zmon j M1) l);
      case (MFactor P2 c (zmon j M1)).
      intros R1 S1 H1.
@@ -986,9 +884,9 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
      apply radd_ext; rsimpl.
      rewrite (ARadd_comm ARth); rsimpl.
      rewrite zmon_pred_ok;rsimpl.
-   intros j M1.
-     case_eq (i ?= j); intros He; simpl.
-       rewrite (Pos.compare_eq _ _ He).
+   + intros j M1.
+     case Pos.compare_spec; intros He; simpl.
+     * rewrite 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.
@@ -1002,7 +900,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
        repeat (rewrite <-(ARmul_assoc ARth)).
        apply rmul_ext; rsimpl.
        rewrite (ARmul_comm ARth); rsimpl.
-       generalize (Hrec1 (c, vmon (j - i) M1) l);
+     * generalize (Hrec1 (c, vmon (j - i) M1) l);
              case (MFactor P2 c (vmon (j - i) M1));
         simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
        rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto.
@@ -1018,9 +916,9 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
        rewrite <- (ARmul_comm ARth (Mphi (tail l) M1)); rsimpl.
        repeat (rewrite <-(ARmul_assoc ARth)).
        apply rmul_ext; rsimpl.
-       rewrite <- pow_pos_Pplus.
-       rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl.
-       generalize (Hrec1 (c, mkZmon 1 M1) l);
+       rewrite <- pow_pos_add.
+       rewrite Pos.add_comm, Pos.sub_add by trivial; rsimpl.
+     * generalize (Hrec1 (c, mkZmon 1 M1) l);
              case (MFactor P2 c (mkZmon 1 M1));
         simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
        rewrite H; rsimpl.
@@ -1041,12 +939,10 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
        rewrite (ARmul_comm ARth); rsimpl.
        repeat (rewrite <- (ARmul_assoc ARth)).
        apply rmul_ext; rsimpl.
-       rewrite <- pow_pos_Pplus.
-       rewrite (Pplus_minus _ _ He); rsimpl.
+       rewrite <- pow_pos_add.
+       rewrite Pos.add_comm, Pos.sub_add by trivial; rsimpl.
  Qed.
 
-(* Proof for the symmetric version *)
-
  Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
     POneSubst P1 M1 P2 = Some P3 -> phi (fst M1) * Mphi l (snd M1) == P2@l -> P1@l == P3@l.
  Proof.
@@ -1070,30 +966,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    injection H2; intros; subst;trivial.
   rewrite H;rewrite Padd_ok;rewrite Pmul_ok;rsimpl.
  Qed.
-(*
-  Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
-    POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
-Proof.
- intros P2 M1 P3 P4 l; unfold POneSubst.
- generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
- intros Q1 R1; case R1.
-   intros c H; rewrite H.
-   generalize (morph_eq CRmorph c cO);
-        case (c ?=! cO); simpl; auto.
-   intros H1 H2; rewrite H1; auto; rsimpl.
-   discriminate.
-   intros _ H1 H2; injection H1; intros; subst.
-   rewrite H2; rsimpl.
-  rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
-  intros i P5 H; rewrite H.
-   intros HH H1; injection HH; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite Pmul_ok. rewrite H1; rsimpl.
-   intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
-   injection H2; intros; subst; rsimpl.
-   rewrite Padd_ok.
-   rewrite Pmul_ok; rsimpl.
- Qed.
-*)
+
  Lemma PNSubst1_ok: forall n P1 M1 P2 l,
     [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
  Proof.
@@ -1193,47 +1066,16 @@ Strategy expand [PEeval].
  Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
  Proof.
   destruct p;simpl;intros;Esimpl;trivial.
-  rewrite <-jump_tl;rewrite nth_jump;rrefl.
+  rewrite <-jump_tl;rewrite nth_jump;reflexivity.
   rewrite <- nth_jump.
-  rewrite nth_Pdouble_minus_one;rrefl.
+  rewrite nth_pred_double;reflexivity.
  Qed.
 
  Ltac Esimpl3 :=
   repeat match goal with
   | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l)
   | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l)
-  end;Esimpl2;try rrefl;try apply (ARadd_comm ARth).
-
-(* Power using the chinise algorithm *)
-(*Section POWER.
-  Variable subst_l : Pol -> Pol.
-  Fixpoint Ppow_pos (P:Pol) (p:positive){struct p} : Pol :=
-   match p with
-   | xH => P
-   | xO p => subst_l (Psquare (Ppow_pos P p))
-   | xI p => subst_l (Pmul P (Psquare (Ppow_pos P p)))
-   end.
-
-  Definition Ppow_N P n :=
-   match n with
-   | N0 => P1
-   | Npos p => Ppow_pos P p
-   end.
-
-  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
-         forall P p, (Ppow_pos P p)@l == (pow_pos Pmul P p)@l.
-  Proof.
-   intros l subst_l_ok P.
-   induction p;simpl;intros;try rrefl;try rewrite subst_l_ok.
-   repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl.
-   repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl.
-  Qed.
-
-  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
-         forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
-  Proof.  destruct n;simpl. rrefl. apply Ppow_pos_ok. trivial.  Qed.
-
- End POWER. *)
+  end;Esimpl2;try reflexivity;try apply (ARadd_comm ARth).
 
 Section POWER.
   Variable subst_l : Pol -> Pol.
@@ -1255,12 +1097,12 @@ Section POWER.
   Proof.
    intros l subst_l_ok res P p. generalize res;clear res.
    induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp.
-   rsimpl. mul_push (P@l);rsimpl. rsimpl. rrefl.
+   rsimpl. mul_push (P@l);rsimpl. rsimpl. reflexivity.
   Qed.
 
   Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
          forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
-  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl.  Qed.
+  Proof.  destruct n;simpl. reflexivity. rewrite Ppow_pos_ok by trivial. Esimpl.  Qed.
 
  End POWER.
 
@@ -1289,42 +1131,6 @@ Section POWER.
 
   Definition norm_subst pe := subst_l (norm_aux pe).
 
- (*
-  Fixpoint norm_subst (pe:PExpr) : Pol :=
-   match pe with
-   | PEc c => Pc c
-   | PEX j => subst_l (mk_X j)
-   | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1)
-   | PEadd pe1 (PEopp pe2) =>
-     Psub (norm_subst pe1) (norm_subst pe2)
-   | PEadd pe1 pe2 => Padd (norm_subst  pe1) (norm_subst pe2)
-   | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2)
-   | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2)
-   | PEopp pe1 => Popp (norm_subst pe1)
-   | PEpow pe1 n => Ppow_subst (norm_subst pe1) n
-   end.
-
-  Lemma norm_subst_spec :
-     forall l pe, MPcond lmp l ->
-       PEeval l pe == (norm_subst pe)@l.
-  Proof.
-   intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l).
-      unfold subst_l;intros.
-      rewrite <- PNSubstL_ok;trivial. rrefl.
-   assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l).
-    intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl.
-   induction pe;simpl;Esimpl3.
-   rewrite subst_l_ok;apply mkX_ok.
-   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3.
-   rewrite IHpe1;rewrite IHpe2;rrefl.
-   rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl.
-   rewrite IHpe;rrefl.
-   unfold Ppow_subst. rewrite Ppow_N_ok. trivial.
-   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
-   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;rrefl.
-  Qed.
-*)
  Lemma norm_aux_spec :
      forall l pe, MPcond lmp l ->
        PEeval l pe == (norm_aux pe)@l.
@@ -1333,13 +1139,13 @@ Section POWER.
    induction pe;simpl;Esimpl3.
    apply mkX_ok.
    rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3.
-   rewrite IHpe1;rewrite IHpe2;rrefl.
-   rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
-   rewrite IHpe;rrefl.
-   rewrite Ppow_N_ok by (intros;rrefl).
+   rewrite IHpe1;rewrite IHpe2;reflexivity.
+   rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
+   rewrite IHpe;reflexivity.
+   rewrite Ppow_N_ok by (intros;reflexivity).
    rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
    induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;rrefl.
+      repeat rewrite Pmul_ok;reflexivity.
   Qed.
 
  Lemma norm_subst_spec :
@@ -1519,7 +1325,7 @@ Section POWER.
    | Pinj j Q =>
      add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
    | PX P i Q =>
-     let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in
+     let rP := add_mult_dev rP P fv (N.add (Npos i) n) lm in
      if Q ?== P0 then rP
      else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm)
    end.
@@ -1531,7 +1337,7 @@ Section POWER.
   | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm)
   | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
   | PX P i Q =>
-     let rP := mult_dev P fv (Nplus (Npos i) n) lm in
+     let rP := mult_dev P fv (N.add (Npos i) n) lm in
      if Q ?== P0 then rP
      else
        let lmq := add_pow_list (hd 0 fv) n lm in
@@ -1575,7 +1381,7 @@ Section POWER.
     (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l).
    induction l;intros;simpl;Esimpl.
    destruct a;rewrite IHl;Esimpl.
-   rewrite (ARmul_comm ARth (pow_pos rmul r p)). rrefl.
+   rewrite (ARmul_comm ARth (pow_pos rmul r p)). reflexivity.
   intros;unfold rev'. rewrite H;simpl;Esimpl.
   Qed.
 
@@ -1630,13 +1436,13 @@ Qed.
    change match n with
     | N0 => Npos p
     | Npos q => Npos (p + q)
-    end with (Nplus (Npos p) n);trivial.
+    end with (N.add (Npos p) n);trivial.
    assert (H := Peq_ok P3 P0).
     destruct (P3 ?== P0).
-    rewrite (H (refl_equal true)).
-   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+    rewrite (H (eq_refl true)).
+   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
    rewrite  IHP2.
-   rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+   rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
  Qed.
 
  Lemma mult_dev_ok : forall P fv n lm,
@@ -1653,13 +1459,13 @@ Qed.
    change match n with
     | N0 => Npos p
     | Npos q => Npos (p + q)
-    end with (Nplus (Npos p) n);trivial.
+    end with (N.add (Npos p) n);trivial.
    assert (H := Peq_ok P3 P0).
     destruct (P3 ?== P0).
-    rewrite (H (refl_equal true)).
-   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+    rewrite (H (eq_refl true)).
+   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
    rewrite add_mult_dev_ok. rewrite IHP1; rewrite add_pow_list_ok.
-   destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+   destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
   Qed.
 
  Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P  == P@fv.
@@ -1687,7 +1493,7 @@ Qed.
 
  Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P  == P@fv.
  Proof.
-  unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;rrefl.
+  unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;reflexivity.
  Qed.
 
  Lemma ring_rw_pow_correct : forall n lH l,
@@ -1711,14 +1517,14 @@ Qed.
   Definition mkpow x p :=
     match p with
     | xH => x
-    | xO p => mkmult_pow x x (Pdouble_minus_one p)
+    | xO p => mkmult_pow x x (Pos.pred_double p)
     | xI p => mkmult_pow x x (xO p)
     end.
 
   Definition mkopp_pow x p :=
     match p with
     | xH => -x
-    | xO p => mkmult_pow (-x) x (Pdouble_minus_one p)
+    | xO p => mkmult_pow (-x) x (Pos.pred_double p)
     | xI p => mkmult_pow (-x) x (xO p)
     end.
 
@@ -1737,9 +1543,9 @@ Qed.
     repeat rewrite mkmult_pow_ok;Esimpl.
     rewrite mkmult_pow_ok;Esimpl.
     pattern x at 1;replace x with (pow_pos rmul x 1).
-    rewrite <- pow_pos_Pplus.
-    rewrite <- Pplus_one_succ_l.
-    rewrite Psucc_o_double_minus_one_eq_xO.
+    rewrite <- pow_pos_add.
+    rewrite Pos.add_1_l.
+    rewrite Pos.succ_pred_double.
     simpl;Esimpl.
     trivial.
   Qed.
@@ -1750,9 +1556,9 @@ Qed.
     repeat rewrite mkmult_pow_ok;Esimpl.
     rewrite mkmult_pow_ok;Esimpl.
     pattern x at 1;replace x with (pow_pos rmul x 1).
-    rewrite <- pow_pos_Pplus.
-    rewrite <- Pplus_one_succ_l.
-    rewrite Psucc_o_double_minus_one_eq_xO.
+    rewrite <- pow_pos_add.
+    rewrite Pos.add_1_l.
+    rewrite Pos.succ_pred_double.
     simpl;Esimpl.
     trivial.
   Qed.
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index d33e9a82a..7a7ffcfdc 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -3,6 +3,7 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import Ring_polynom.
 Require Import BinList.
+Require Export ListTactics.
 Require Import InitialRing.
 Require Import Quote.
 Declare ML Module "newring_plugin".
@@ -14,7 +15,7 @@ Ltac compute_assertion eqn t' t :=
   let nft := eval vm_compute in t in
   pose (t' := nft);
   assert (eqn : t = t');
-  [vm_cast_no_check (refl_equal t')|idtac].
+  [vm_cast_no_check (eq_refl t')|idtac].
 
 Ltac relation_carrier req :=
   let ty := type of req in
@@ -340,7 +341,7 @@ Ltac Ring RNG lemma lH :=
         || idtac "can not automatically proof hypothesis :";
            idtac " maybe a left member of a hypothesis is not a monomial")
     | vm_compute;
-      (exact (refl_equal true) || fail "not a valid ring equation")]).
+      (exact (eq_refl true) || fail "not a valid ring equation")]).
 
 Ltac Ring_norm_gen f RNG lemma lH rl :=
   let mkFV := get_RingFV RNG in
@@ -385,7 +386,7 @@ Ltac Ring_simplify_gen f RNG lH rl :=
   let lemma := get_SimplifyLemma RNG in
   let l := fresh "to_rewrite" in
   pose (l:= rl);
-  generalize (refl_equal l);
+  generalize (eq_refl l);
   unfold l at 2;
   get_Pre RNG ();
   let rl :=
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index ab9925528..f1f419662 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Setoid.
-Require Import BinPos.
-Require Import BinNat.
+Require Import Setoid Morphisms BinPos BinNat.
 
 Set Implicit Arguments.
 
@@ -35,48 +33,42 @@ Section Power.
  Variable rI : R.
  Variable rmul : R -> R -> R.
  Variable req : R -> R -> Prop.
- Variable Rsth : Setoid_Theory R req.
- Notation "x * y " := (rmul x y).
- Notation "x == y" := (req x y).
+ Variable Rsth : Equivalence req.
+ Infix "*" := rmul.
+ Infix "==" := req.
 
- Hypothesis mul_ext :
-   forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2.
- Hypothesis mul_comm : forall x y, x * y == y * x.
+ Hypothesis mul_ext : Proper (req ==> req ==> req) rmul.
  Hypothesis mul_assoc  : forall x y z, x * (y * z) == (x * y) * z.
- Add Setoid R req Rsth as R_set_Power.
- Add Morphism rmul : rmul_ext_Power. exact mul_ext. Qed.
 
-
- Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
+ Fixpoint pow_pos (x:R) (i:positive) : R :=
   match i with
   | xH => x
-  | xO i => let p := pow_pos x i in rmul p p
-  | xI i => let p := pow_pos x i in rmul x (rmul p p)
+  | xO i => let p := pow_pos x i in p * p
+  | xI i => let p := pow_pos x i in x * (p * p)
   end.
 
- Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Lemma pow_pos_swap x j : pow_pos x j * x == x * pow_pos x j.
  Proof.
-  induction j;simpl.
-  rewrite IHj.
-  rewrite (mul_comm x (pow_pos x j *pow_pos x j)).
-  setoid_rewrite (mul_comm x (pow_pos x j)) at 2.
-  repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
-  repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
-  apply (Seq_refl _ _ Rsth).
+  induction j; simpl; rewrite <- ?mul_assoc.
+  - f_equiv. now do 2 (rewrite IHj, mul_assoc).
+  - now do 2 (rewrite IHj, mul_assoc).
+  - reflexivity.
  Qed.
 
- Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Lemma pow_pos_succ x j :
+   pow_pos x (Pos.succ j) == x * pow_pos x j.
  Proof.
-  intro x;induction i;intros.
-  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat rewrite IHi.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc.
-  simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc;
-   simpl. apply (Seq_refl _ _ Rsth).
+  induction j; simpl; try reflexivity.
+  rewrite IHj, <- mul_assoc; f_equiv.
+  now rewrite mul_assoc, pow_pos_swap, mul_assoc.
+ Qed.
+
+ Lemma pow_pos_add x i j :
+   pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+  induction i using Pos.peano_ind.
+  - now rewrite Pos.add_1_l, pow_pos_succ.
+  - now rewrite Pos.add_succ_l, !pow_pos_succ, IHi, mul_assoc.
  Qed.
 
  Definition pow_N (x:R) (p:N) :=
@@ -87,9 +79,9 @@ Section Power.
 
  Definition id_phi_N (x:N) : N := x.
 
- Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.
+ Lemma pow_N_pow_N x n : pow_N x (id_phi_N n) == pow_N x n.
  Proof.
-  intros; apply (Seq_refl _ _ Rsth).
+  reflexivity.
  Qed.
 
 End Power.
@@ -98,19 +90,18 @@ Section DEFINITIONS.
  Variable R : Type.
  Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
  Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
+ Notation "0" := rO.  Notation "1" := rI.
+ Infix "==" := req. Infix "+" := radd. Infix "*" := rmul.
+ Infix "-" := rsub. Notation "- x" := (ropp x).
 
  (** Semi Ring *)
  Record semi_ring_theory : Prop := mk_srt {
     SRadd_0_l   : forall n, 0 + n == n;
-    SRadd_comm   : forall n m, n + m == m + n ;
+    SRadd_comm  : forall n m, n + m == m + n ;
     SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
     SRmul_1_l   : forall n, 1*n == n;
     SRmul_0_l   : forall n, 0*n == 0;
-    SRmul_comm   : forall n m, n*m == m*n;
+    SRmul_comm  : forall n m, n*m == m*n;
     SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
     SRdistr_l   : forall n m p, (n + m)*p == n*p + m*p
   }.
@@ -119,11 +110,11 @@ Section DEFINITIONS.
 (*Almost ring are no ring : Ropp_def is missing **)
  Record almost_ring_theory : Prop := mk_art {
     ARadd_0_l   : forall x, 0 + x == x;
-    ARadd_comm   : forall x y, x + y == y + x;
+    ARadd_comm  : forall x y, x + y == y + x;
     ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z;
     ARmul_1_l   : forall x, 1 * x == x;
     ARmul_0_l   : forall x, 0 * x == 0;
-    ARmul_comm   : forall x y, x * y == y * x;
+    ARmul_comm  : forall x y, x * y == y * x;
     ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z;
     ARdistr_l   : forall x y z, (x + y) * z == (x * z) + (y * z);
     ARopp_mul_l : forall x y, -(x * y) == -x * y;
@@ -134,10 +125,10 @@ Section DEFINITIONS.
  (** Ring *)
  Record ring_theory : Prop := mk_rt {
     Radd_0_l    : forall x, 0 + x == x;
-    Radd_comm    : forall x y, x + y == y + x;
+    Radd_comm   : forall x y, x + y == y + x;
     Radd_assoc  : forall x y z, x + (y + z) == (x + y) + z;
     Rmul_1_l    : forall x, 1 * x == x;
-    Rmul_comm    : forall x y, x * y == y * x;
+    Rmul_comm   : forall x y, x * y == y * x;
     Rmul_assoc  : forall x y z, x * (y * z) == (x * y) * z;
     Rdistr_l    : forall x y z, (x + y) * z == (x * z) + (y * z);
     Rsub_def    : forall x y, x - y == x + -y;
@@ -148,19 +139,15 @@ Section DEFINITIONS.
 
  Record sring_eq_ext : Prop := mk_seqe {
     (* SRing operators are compatible with equality *)
-    SRadd_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2;
-    SRmul_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2
+    SRadd_ext : Proper (req ==> req ==> req) radd;
+    SRmul_ext : Proper (req ==> req ==> req) rmul
   }.
 
  Record ring_eq_ext : Prop := mk_reqe {
     (* Ring operators are compatible with equality *)
-    Radd_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2;
-    Rmul_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2;
-    Ropp_ext : forall x1 x2, x1 == x2 ->  -x1 == -x2
+    Radd_ext : Proper (req ==> req ==> req) radd;
+    Rmul_ext : Proper (req ==> req ==> req) rmul;
+    Ropp_ext : Proper (req ==> req) ropp
   }.
 
  (** Interpretation morphisms definition*)
@@ -170,9 +157,9 @@ Section DEFINITIONS.
  Variable ceqb : C->C->bool.
  (* [phi] est un morphisme de [C] dans [R] *)
  Variable phi : C -> R.
- Notation "x +! y" := (cadd x y). Notation "x -! y " := (csub x y).
- Notation "x *! y " := (cmul x y). Notation "-! x" := (copp x).
- Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
+ Infix "+!" := cadd. Infix "-!" := csub.
+ Infix "*!" := cmul. Notation "-! x" := (copp x).
+ Infix "?=!" := ceqb. Notation "[ x ]" := (phi x).
 
 (*for semi rings*)
  Record semi_morph : Prop := mkRmorph {
@@ -216,15 +203,13 @@ Section DEFINITIONS.
  End MORPHISM.
 
  (** Identity is a morphism *)
- Variable Rsth : Setoid_Theory R req.
-   Add Setoid R req Rsth as R_setoid1.
+ Variable Rsth : Equivalence req.
  Variable reqb : R->R->bool.
  Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y.
  Definition IDphi (x:R) := x.
  Lemma IDmorph : ring_morph rO rI radd rmul rsub ropp reqb IDphi.
  Proof.
-  apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi);intros;unfold IDphi;
-  try apply (Seq_refl _ _ Rsth);auto.
+  now apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi).
  Qed.
 
  (** Specification of the power function *)
@@ -239,35 +224,31 @@ Section DEFINITIONS.
 
  End POWER.
 
- Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth).
+ Definition pow_N_th :=
+   mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth).
 
 
 End DEFINITIONS.
 
-
-
 Section ALMOST_RING.
  Variable R : Type.
  Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
  Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
+ Notation "0" := rO.  Notation "1" := rI.
+ Infix "==" := req. Infix "+" := radd.  Infix "* " := rmul.
+ Infix "-" := rsub. Notation "- x" := (ropp x).
 
  (** Leibniz equality leads to a setoid theory and is extensional*)
- Lemma Eqsth : Setoid_Theory R (@eq R).
- Proof.  constructor;red;intros;subst;trivial. Qed.
+ Lemma Eqsth : Equivalence (@eq R).
+ Proof. exact eq_equivalence. Qed.
 
  Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R).
- Proof. constructor;intros;subst;trivial. Qed.
+ Proof. constructor;solve_proper. Qed.
 
  Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R).
- Proof. constructor;intros;subst;trivial. Qed.
+ Proof. constructor;solve_proper. Qed.
 
- Variable Rsth : Setoid_Theory R req.
-   Add Setoid R req Rsth as R_setoid2.
-   Ltac sreflexivity := apply (Seq_refl _ _ Rsth).
+ Variable Rsth : Equivalence req.
 
  Section SEMI_RING.
  Variable SReqe : sring_eq_ext radd rmul req.
@@ -282,23 +263,24 @@ Section ALMOST_RING.
  Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y).
 
  Lemma SRopp_ext : forall x y, x == y -> -x == -y.
- Proof. intros x y H;exact H. Qed.
+ Proof. intros x y H; exact H. Qed.
 
  Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req.
  Proof.
-  constructor.  exact (SRadd_ext SReqe). exact (SRmul_ext SReqe).
-  exact SRopp_ext.
+  constructor.
+  - exact (SRadd_ext SReqe).
+  - exact (SRmul_ext SReqe).
+  - exact SRopp_ext.
  Qed.
 
  Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y.
- Proof. intros;sreflexivity. Qed.
+ Proof. reflexivity. Qed.
 
  Lemma SRopp_add : forall x y, -(x + y) == -x + -y.
- Proof. intros;sreflexivity.  Qed.
-
+ Proof. reflexivity. Qed.
 
  Lemma SRsub_def   : forall x y, x - y == x + -y.
- Proof. intros;sreflexivity. Qed.
+ Proof. reflexivity. Qed.
 
  Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req.
  Proof (mk_art 0 1 radd rmul SRsub SRopp req
@@ -315,7 +297,7 @@ Section ALMOST_RING.
  Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req
                             0 1 radd rmul SRsub SRopp reqb (@IDphi R).
  Proof.
-  apply mkmorph;intros;try sreflexivity.  unfold IDphi;auto.
+  now apply mkmorph.
  Qed.
 
  (* a semi_morph can be extended to a ring_morph for the almost_ring derived
@@ -331,9 +313,7 @@ Section ALMOST_RING.
    ring_morph rO rI radd rmul SRsub SRopp req
               cO cI cadd cmul cadd (fun x => x) ceqb phi.
  Proof.
- case Smorph; intros; constructor; auto.
- unfold SRopp in |- *; intros.
-  setoid_reflexivity.
+ case Smorph; now constructor.
  Qed.
 
  End  SEMI_RING.
@@ -347,31 +327,28 @@ Section ALMOST_RING.
  Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
 
  (** Rings are almost rings*)
- Lemma Rmul_0_l : forall x, 0 * x == 0.
+ Lemma Rmul_0_l x : 0 * x == 0.
  Proof.
-  intro x; setoid_replace (0*x) with ((0+1)*x + -x).
-  rewrite (Radd_0_l Rth); rewrite (Rmul_1_l Rth).
-  rewrite (Ropp_def Rth);sreflexivity.
+  setoid_replace (0*x) with ((0+1)*x + -x).
+  now rewrite (Radd_0_l Rth), (Rmul_1_l Rth), (Ropp_def Rth).
 
-  rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth).
-  rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth).
-  rewrite (Radd_comm Rth); rewrite (Radd_0_l Rth);sreflexivity.
+  rewrite (Rdistr_l Rth), (Rmul_1_l Rth).
+  rewrite <- (Radd_assoc Rth), (Ropp_def Rth).
+  now rewrite (Radd_comm Rth), (Radd_0_l Rth).
  Qed.
 
- Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y.
+ Lemma Ropp_mul_l x y : -(x * y) == -x * y.
  Proof.
-  intros x y;rewrite <-(Radd_0_l Rth (- x * y)).
-  rewrite (Radd_comm Rth).
-  rewrite <-(Ropp_def Rth (x*y)).
-  rewrite (Radd_assoc Rth).
-  rewrite <- (Rdistr_l Rth).
-  rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth).
-  rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity.
+  rewrite <-(Radd_0_l Rth (- x * y)).
+  rewrite (Radd_comm Rth), <-(Ropp_def Rth (x*y)).
+  rewrite (Radd_assoc Rth), <- (Rdistr_l Rth).
+  rewrite (Rth.(Radd_comm) (-x)), (Ropp_def Rth).
+  now rewrite Rmul_0_l, (Radd_0_l Rth).
  Qed.
 
- Lemma Ropp_add : forall x y, -(x + y) == -x + -y.
+ Lemma Ropp_add x y : -(x + y) == -x + -y.
  Proof.
-  intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))).
+  rewrite <- ((Radd_0_l Rth) (-(x+y))).
   rewrite <- ((Ropp_def Rth) x).
   rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))).
   rewrite <- ((Ropp_def Rth) y).
@@ -383,17 +360,17 @@ Section ALMOST_RING.
   rewrite ((Radd_comm Rth) y).
   rewrite <- ((Radd_assoc Rth)  (- x)).
   rewrite ((Radd_assoc Rth) y).
-  rewrite ((Radd_comm Rth) y);rewrite (Ropp_def Rth).
-  rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth).
-  apply (Radd_comm Rth).
+  rewrite ((Radd_comm Rth) y), (Ropp_def Rth).
+  rewrite ((Radd_comm Rth) (-x) 0), (Radd_0_l Rth).
+  now apply (Radd_comm Rth).
  Qed.
 
- Lemma Ropp_opp : forall x, - -x == x.
+ Lemma Ropp_opp x : - -x == x.
  Proof.
-  intros x; rewrite <- (Radd_0_l Rth (- -x)).
+  rewrite <- (Radd_0_l Rth (- -x)).
   rewrite <- (Ropp_def Rth x).
-  rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth).
-  rewrite ((Radd_comm Rth) x);apply (Radd_0_l Rth).
+  rewrite <- (Radd_assoc Rth), (Ropp_def Rth).
+  rewrite ((Radd_comm Rth) x); now apply (Radd_0_l Rth).
  Qed.
 
  Lemma  Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
@@ -407,10 +384,10 @@ Section ALMOST_RING.
  Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C).
  Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool).
  Variable phi : C -> R.
-  Notation "x +! y" := (cadd x y).  Notation "x *! y " := (cmul x y).
-  Notation "x -! y " := (csub x y).  Notation "-! x" := (copp x).
-  Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
- Variable Csth : Setoid_Theory C ceq.
+  Infix "+!" := cadd. Infix "*!" := cmul.
+  Infix "-!" := csub. Notation "-! x" := (copp x).
+  Notation "?=!" := ceqb. Notation "[ x ]" := (phi x).
+ Variable Csth : Equivalence ceq.
  Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
    Add Setoid C ceq Csth as C_setoid.
    Add Morphism cadd : cadd_ext.  exact (Radd_ext Ceqe). Qed.
@@ -420,9 +397,9 @@ Section ALMOST_RING.
  Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi.
  Variable phi_ext : forall x y, ceq x y -> [x] == [y].
    Add Morphism phi : phi_ext1.  exact phi_ext. Qed.
- Lemma Smorph_opp : forall x, [-!x] == -[x].
+ Lemma Smorph_opp x : [-!x] == -[x].
  Proof.
-  intros x;rewrite <-  (Rth.(Radd_0_l) [-!x]).
+  rewrite <-  (Rth.(Radd_0_l) [-!x]).
   rewrite <- ((Ropp_def Rth) [x]).
   rewrite ((Radd_comm Rth) [x]).
   rewrite <- (Radd_assoc Rth).
@@ -430,17 +407,18 @@ Section ALMOST_RING.
   rewrite (Ropp_def Cth).
   rewrite (Smorph0 Smorph).
   rewrite (Radd_comm Rth (-[x])).
-  apply (Radd_0_l Rth);sreflexivity.
+  now apply (Radd_0_l Rth).
  Qed.
 
- Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y].
+ Lemma Smorph_sub x y : [x -! y] == [x] - [y].
  Proof.
-  intros x y; rewrite (Rsub_def Cth);rewrite (Rsub_def Rth).
-  rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity.
+  rewrite (Rsub_def Cth), (Rsub_def Rth).
+  now rewrite (Smorph_add Smorph), Smorph_opp.
  Qed.
 
- Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req
-                                             cO cI cadd cmul csub copp ceqb phi.
+ Lemma Smorph_morph :
+   ring_morph 0 1 radd rmul rsub ropp req
+     cO cI cadd cmul csub copp ceqb phi.
  Proof
   (mkmorph 0 1 radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi
         (Smorph0 Smorph) (Smorph1 Smorph)
@@ -458,17 +436,11 @@ elim ARth; intros.
 constructor; trivial.
 Qed.
 
- Lemma ARsub_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+ Instance ARsub_ext : Proper (req ==> req ==> req) rsub.
  Proof.
-  intros.
-  setoid_replace (x1 - y1) with (x1 + -y1).
-  setoid_replace (x2 - y2) with (x2 + -y2).
-  rewrite H;rewrite H0;sreflexivity.
-  apply (ARsub_def ARth).
-  apply (ARsub_def ARth).
+  intros x1 x2 Ex y1 y2 Ey.
+  now rewrite !(ARsub_def ARth), Ex, Ey.
  Qed.
-   Add Morphism rsub : rsub_ext.  exact ARsub_ext. Qed.
 
  Ltac mrewrite :=
    repeat first
@@ -479,64 +451,56 @@ Qed.
      | rewrite (ARmul_0_l ARth)
      | rewrite <- ((ARmul_comm ARth) 0)
      | rewrite (ARdistr_l ARth)
-     | sreflexivity
+     | reflexivity
      | match goal with
        | |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y))
        end].
 
- Lemma ARadd_0_r : forall x, (x + 0) == x.
- Proof. intros; mrewrite. Qed.
+ Lemma ARadd_0_r x : x + 0 == x.
+ Proof. mrewrite. Qed.
 
- Lemma ARmul_1_r   : forall x, x * 1 == x.
- Proof. intros;mrewrite. Qed.
+ Lemma ARmul_1_r x : x * 1 == x.
+ Proof. mrewrite. Qed.
 
- Lemma ARmul_0_r : forall x, x * 0 == 0.
- Proof. intros;mrewrite. Qed.
+ Lemma ARmul_0_r x : x * 0 == 0.
+ Proof. mrewrite. Qed.
 
- Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y.
+ Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y.
  Proof.
-  intros;mrewrite.
-  repeat rewrite (ARth.(ARmul_comm) z);sreflexivity.
+  mrewrite. now rewrite !(ARth.(ARmul_comm) z).
  Qed.
 
- Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x.
  Proof.
-  intros;rewrite <-(ARth.(ARadd_assoc) x).
-  rewrite (ARth.(ARadd_comm) x);sreflexivity.
+  now rewrite <-(ARth.(ARadd_assoc) x), (ARth.(ARadd_comm) x).
  Qed.
 
- Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
+ Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x.
  Proof.
-  intros; repeat rewrite <- (ARadd_assoc ARth);
-   rewrite ((ARadd_comm ARth) x); sreflexivity.
+  now rewrite <- !(ARadd_assoc ARth), ((ARadd_comm ARth) x).
  Qed.
 
- Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x.
+ Lemma ARmul_assoc1 x y z : (x * y) * z == (y * z) * x.
  Proof.
-  intros;rewrite <-((ARmul_assoc ARth) x).
-  rewrite ((ARmul_comm ARth) x);sreflexivity.
+  now rewrite <- ((ARmul_assoc ARth) x), ((ARmul_comm ARth) x).
  Qed.
 
- Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x.
+ Lemma ARmul_assoc2 x y z : (y * x) * z == (y * z) * x.
  Proof.
-  intros; repeat rewrite <- (ARmul_assoc ARth);
-   rewrite ((ARmul_comm ARth) x); sreflexivity.
+  now rewrite <- !(ARmul_assoc ARth), ((ARmul_comm ARth) x).
  Qed.
 
- Lemma ARopp_mul_r : forall x y,  - (x * y) == x * -y.
+ Lemma ARopp_mul_r x y : - (x * y) == x * -y.
  Proof.
-  intros;rewrite ((ARmul_comm ARth) x y);
-   rewrite (ARopp_mul_l ARth); apply (ARmul_comm ARth).
+  rewrite ((ARmul_comm ARth) x y), (ARopp_mul_l ARth).
+  now apply (ARmul_comm ARth).
  Qed.
 
  Lemma ARopp_zero : -0 == 0.
  Proof.
-  rewrite <- (ARmul_0_r 0); rewrite (ARopp_mul_l ARth).
-  repeat rewrite ARmul_0_r; sreflexivity.
+  now rewrite <- (ARmul_0_r 0), (ARopp_mul_l ARth), !ARmul_0_r.
  Qed.
 
-
-
 End ALMOST_RING.
 
 
@@ -611,6 +575,8 @@ Ltac gen_add_push add Rsth Reqe ARth x :=
      progress rewrite (ARadd_assoc2 Rsth Reqe ARth x y z)
   | |- context [add (add x ?y) ?z] =>
      progress rewrite (ARadd_assoc1 Rsth ARth x y z)
+  | |- context [(add x ?y)] =>
+     progress rewrite (ARadd_comm ARth x y)
   end).
 
 Ltac gen_mul_push mul Rsth Reqe ARth x :=
@@ -619,5 +585,6 @@ Ltac gen_mul_push mul Rsth Reqe ARth x :=
      progress rewrite (ARmul_assoc2 Rsth Reqe ARth x y z)
   | |- context [mul (mul x ?y) ?z] =>
      progress rewrite (ARmul_assoc1 Rsth ARth x y z)
+  | |- context [(mul x ?y)] =>
+     progress rewrite (ARmul_comm ARth x y)
   end).
-
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index 889048653..58a4d7ea6 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -3,7 +3,7 @@ Require Export Integral_domain.
 Require Export Ncring_initial.
 
 Instance Zcri: (Cring (Rr:=Zr)).
-red. exact Zmult_comm. Defined.
+red. exact Z.mul_comm. Defined.
 
 Lemma Z_one_zero: 1%Z <> 0%Z.
 omega. 
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index d3ed36ee9..281ffa229 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -39,14 +39,14 @@ Ltac Zpower_neg :=
   repeat match goal with
   | [|- ?G] =>
     match G with
-    | context c [Zpower _ (Zneg _)] =>
+    | context c [Z.pow _ (Zneg _)] =>
       let t := context c [Z0] in
       change t
     end
   end.
 
 Add Ring Zr : Zth
-  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ],
    power_tac Zpower_theory [Zpow_tac],
     (* The two following option are not needed, it is the default chose when the set of
         coefficiant is usual ring Z *)