Imported Upstream version 8.4dfsgupstream/8.4dfsg

22 files changed, 1074 insertions, 1480 deletions

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 06822ae1..ed35bb46 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 7128280a..b3c59457 100644
--- a/plugins/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
@@ -1,16 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       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 3d6e53fc..02194d4f 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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.v b/plugins/setoid_ring/Field.v
index 90f2f497..6d454ba8 100644
--- a/plugins/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index da42bbd9..8ac952c0 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 40138526..bc05c252 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1,13 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 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,16 +115,17 @@ 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 *)
 
 Lemma rsub_0_l : forall r, 0 - r == - r.
-intros; rewrite (ARsub_def ARth) in |- *;ring.
+intros; rewrite (ARsub_def ARth);ring.
 Qed.
 
 Lemma rsub_0_r : forall r, r - 0 == r.
-intros; rewrite (ARsub_def ARth) in |- *.
-rewrite (ARopp_zero Rsth Reqe ARth) in |- *;  ring.
+intros; rewrite (ARsub_def ARth).
+rewrite (ARopp_zero Rsth Reqe ARth);  ring.
 Qed.
 
 (***************************************************************************
@@ -135,42 +135,40 @@ Qed.
   ***************************************************************************)
 
 Theorem rdiv_simpl: forall p q, ~ q == 0 ->  q * (p / q) == p.
+Proof.
 intros p q H.
-rewrite rdiv_def in |- *.
+rewrite rdiv_def.
 transitivity (/ q * q * p); [  ring | idtac ].
-rewrite rinv_l in |- *; auto.
+rewrite rinv_l; 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.
 
@@ -179,15 +177,15 @@ Theorem ropp_neq_0 : forall r,
 intros.
 setoid_replace (- r) with (- (1) * r).
  apply field_is_integral_domain; trivial.
- rewrite <- (ARopp_mul_l ARth) in |- *.
-   rewrite (ARmul_1_l ARth) in |- *.
+ rewrite <- (ARopp_mul_l ARth).
+   rewrite (ARmul_1_l ARth).
    reflexivity.
 Qed.
 
 Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1.
 intros.
-rewrite (AFdiv_def AFth) in |- *.
-rewrite (ARmul_comm ARth) in |- *.
+rewrite (AFdiv_def AFth).
+rewrite (ARmul_comm ARth).
 apply (AFinv_l AFth).
 trivial.
 Qed.
@@ -203,14 +201,14 @@ Theorem rdiv2:
  r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
 Proof.
 intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
+assert (~ r2 * r4 == 0) by (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.
 
 
@@ -225,35 +223,36 @@ assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring).
 assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring).
 assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring).
 assert (HH4: ~ r2 * (r4 * r5) == 0)
-   by complete (repeat apply field_is_integral_domain; trivial).
+   by (repeat apply field_is_integral_domain; trivial).
 apply rmul_reg_l with (r2 * (r4 * r5)); 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 * r5) * (r1 / (r2 * r5)) * r4); [  ring | auto ].
  transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [  ring | auto ].
 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.
 
 
@@ -279,13 +278,13 @@ intros r1 r2 H H0.
 assert (~ r1 / r2 == 0) as Hk.
  intros H1; case H.
    transitivity (r2 * (r1 / r2)); auto.
-   rewrite H1 in |- *;  ring.
+   rewrite H1;  ring.
  apply rmul_reg_l with (r1 / r2); auto.
    transitivity (/ (r1 / r2) * (r1 / r2)); auto.
    transitivity 1; auto.
-   repeat rewrite rdiv_def in |- *.
+   repeat rewrite rdiv_def.
    transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac |  ring ].
-   repeat rewrite rinv_l in |- *; auto.
+   repeat rewrite rinv_l; auto.
 Qed.
 Hint Resolve rdiv6 .
 
@@ -296,11 +295,11 @@ Hint Resolve rdiv6 .
  (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
 Proof.
 intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
+assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
 apply rmul_reg_l with (r2 * r4); trivial.
-rewrite rdiv_simpl in |- *; trivial.
+rewrite rdiv_simpl; trivial.
 transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [  ring | idtac ].
-repeat rewrite rdiv_simpl in |- *; trivial.
+repeat rewrite rdiv_simpl; trivial.
 Qed.
 
  Theorem rdiv4b:
@@ -334,8 +333,8 @@ Theorem rdiv7:
  (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3).
 Proof.
 intros.
-rewrite (rdiv_def (r1 / r2)) in |- *.
-rewrite rdiv6 in |- *; trivial.
+rewrite (rdiv_def (r1 / r2)).
+rewrite rdiv6; trivial.
 apply rdiv4; trivial.
 Qed.
 
@@ -373,14 +372,14 @@ Theorem cross_product_eq : forall r1 r2 r3 r4,
   ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4.
 intros.
 transitivity (r1 / r2 * (r4 / r4)).
- rewrite rdiv_r_r in |- *; trivial.
-   symmetry  in |- *.
+ rewrite rdiv_r_r; trivial.
+   symmetry .
    apply (ARmul_1_r Rsth ARth).
- rewrite rdiv4 in |- *; trivial.
-   rewrite H1 in |- *.
-   rewrite (ARmul_comm ARth r2 r4) in |- *.
-   rewrite <- rdiv4 in |- *; trivial.
-   rewrite rdiv_r_r in |- * by trivial.
+ rewrite rdiv4; trivial.
+   rewrite H1.
+   rewrite (ARmul_comm ARth r2 r4).
+   rewrite <- rdiv4; trivial.
+   rewrite rdiv_r_r by trivial.
   apply (ARmul_1_r Rsth ARth).
 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.
@@ -459,8 +451,8 @@ Theorem NPEadd_correct:
  forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2).
 Proof.
 intros l e1 e2.
-destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl;
+destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect;
+ try (intro eq_c; rewrite eq_c); simpl;try apply eq_refl;
  try (ring [(morph0 CRmorph)]).
  apply (morph_add CRmorph).
 Qed.
@@ -511,9 +503,9 @@ Qed.
 
 Theorem NPEmul_correct : forall l e1 e2,
   NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2).
-induction e1;destruct e2; simpl in |- *;try reflexivity;
+induction e1;destruct e2; simpl;try reflexivity;
  repeat apply ceqb_rect;
- try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity;
+ try (intro eq_c; rewrite eq_c); simpl; try reflexivity;
  try ring [(morph0 CRmorph) (morph1 CRmorph)].
  apply (morph_mul CRmorph).
 case N.eqb_spec; intros H; try rewrite <- H; clear H.
@@ -537,9 +529,9 @@ Definition NPEsub e1 e2 :=
 Theorem NPEsub_correct:
  forall l e1 e2,  NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2).
 intros l e1 e2.
-destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
- try rewrite (morph0 CRmorph) in |- *; try reflexivity;
+destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect;
+ try (intro eq_c; rewrite eq_c); simpl;
+ try rewrite (morph0 CRmorph); try reflexivity;
  try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
 apply (morph_sub CRmorph).
 Qed.
@@ -659,8 +651,8 @@ destruct H; trivial.
 Qed.
 
 Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l1.
-intros l l1 l2; elim l1; simpl app in |- *.
- simpl in |- *; auto.
+intros l l1 l2; elim l1; simpl app.
+ simpl; auto.
  destruct l0; simpl in *.
   destruct l2; firstorder.
   firstorder.
@@ -675,8 +667,8 @@ Qed.
 Definition absurd_PCond := cons (PEc cO) nil.
 
 Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
-unfold absurd_PCond in |- *; simpl in |- *.
-red in |- *; intros.
+unfold absurd_PCond; simpl.
+red; intros.
 apply H.
 apply (morph0 CRmorph).
 Qed.
@@ -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.
@@ -1025,13 +1012,13 @@ Theorem Pcond_Fnorm:
  forall l e,
  PCond l (condition (Fnorm e)) ->  ~ NPEeval l (denum (Fnorm e)) == 0.
 intros l e; elim e.
- simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO.
- simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO.
+ simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
+ simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
  intros e1 Hrec1 e2 Hrec2 Hcond.
    simpl condition in Hcond.
-   simpl denum in |- *.
-   rewrite NPEmul_correct in |- *.
-   simpl in |- *.
+   simpl denum.
+   rewrite NPEmul_correct.
+   simpl.
    apply field_is_integral_domain.
    intros HH; case Hrec1; auto.
      apply PCond_app_inv_l with (1 := Hcond).
@@ -1042,9 +1029,9 @@ intros l e; elim e.
    rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
  intros e1 Hrec1 e2 Hrec2 Hcond.
    simpl condition in Hcond.
-   simpl denum in |- *.
-   rewrite NPEmul_correct in |- *.
-   simpl in |- *.
+   simpl denum.
+   rewrite NPEmul_correct.
+   simpl.
    apply field_is_integral_domain.
    intros HH; case Hrec1; auto.
      apply PCond_app_inv_l with (1 := Hcond).
@@ -1055,9 +1042,9 @@ intros l e; elim e.
    rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
  intros e1 Hrec1 e2 Hrec2 Hcond.
    simpl condition in Hcond.
-   simpl denum in |- *.
-   rewrite NPEmul_correct in |- *.
-   simpl in |- *.
+   simpl denum.
+   rewrite NPEmul_correct.
+   simpl.
    apply field_is_integral_domain.
   intros HH; apply Hrec1.
     apply PCond_app_inv_l with (1 := Hcond).
@@ -1069,17 +1056,17 @@ intros l e; elim e.
     rewrite NPEmul_correct; simpl; rewrite HH; ring.
  intros e1 Hrec1 Hcond.
    simpl condition in Hcond.
-   simpl denum in |- *.
+   simpl denum.
    auto.
  intros e1 Hrec1 Hcond.
    simpl condition in Hcond.
-   simpl denum in |- *.
+   simpl denum.
    apply PCond_cons_inv_l with (1:=Hcond).
  intros e1 Hrec1 e2 Hrec2 Hcond.
    simpl condition in Hcond.
-   simpl denum in |- *.
-   rewrite NPEmul_correct in |- *.
-   simpl in |- *.
+   simpl denum.
+   rewrite NPEmul_correct.
+   simpl.
    apply field_is_integral_domain.
     intros HH; apply Hrec1.
     specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
@@ -1222,9 +1209,9 @@ Theorem Fnorm_crossproduct:
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
-rewrite Fnorm_FEeval_PEeval in |- * by
+rewrite Fnorm_FEeval_PEeval by
  apply PCond_app_inv_l with (1 := Hcond).
- rewrite Fnorm_FEeval_PEeval in |- * by
+ rewrite Fnorm_FEeval_PEeval by
   apply PCond_app_inv_r with (1 := Hcond).
   apply cross_product_eq; trivial.
    apply Pcond_Fnorm.
@@ -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.
@@ -1341,28 +1328,28 @@ Proof.
 intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
   subst nfe1 nfe2 den lmp.
 apply Fnorm_crossproduct; trivial.
-simpl in |- *.
-rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
-rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
-rewrite NPEmul_correct in |- *.
-rewrite NPEmul_correct in |- *.
-simpl in |- *.
-repeat rewrite (ARmul_assoc ARth) in |- *.
+simpl.
+rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
+rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
+rewrite NPEmul_correct.
+rewrite NPEmul_correct.
+simpl.
+repeat rewrite (ARmul_assoc ARth).
 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 |- *.
+rewrite Hcrossprod.
 reflexivity.
 Qed.
 
@@ -1381,28 +1368,28 @@ Proof.
 intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
   subst nfe1 nfe2 den lmp.
 apply Fnorm_crossproduct; trivial.
-simpl in |- *.
-rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
-rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
-rewrite NPEmul_correct in |- *.
-rewrite NPEmul_correct in |- *.
-simpl in |- *.
-repeat rewrite (ARmul_assoc ARth) in |- *.
+simpl.
+rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
+rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
+rewrite NPEmul_correct.
+rewrite NPEmul_correct.
+simpl.
+repeat rewrite (ARmul_assoc ARth).
 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 |- *.
+rewrite Hcrossprod.
 reflexivity.
 Qed.
 
@@ -1522,7 +1509,7 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
 
 Lemma fcons_correct : forall l l1,
   PCond l (Fapp l1 nil) -> PCond l l1.
-induction l1; simpl in |- *; intros.
+induction l1; simpl; intros.
  trivial.
  elim PCond_fcons_inv with (1 := H); intros.
    destruct l1; auto.
@@ -1603,7 +1590,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
    simpl in H1.
    case (H _ H1); intros H2 H3.
    case (H0 _ H3); intros H4 H5; split; auto.
-   simpl in |- *.
+   simpl.
    apply field_is_integral_domain; trivial.
    simpl;intros. rewrite pow_th.(rpow_pow_N).
    destruct (H _ H0);split;auto.
@@ -1631,7 +1618,7 @@ generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
 generalize (@ceqb_complete c1 c2).
 case (c1 ?=! c2); auto; intros.
 apply X0.
-red in |- *; intro.
+red; intro.
 absurd (false = true); auto;  discriminate.
 Qed.
 
@@ -1647,18 +1634,18 @@ Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
 Theorem PFcons1_fcons_inv:
   forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
 intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
- simpl in |- *; intros c l1.
+ simpl; intros c l1.
    apply ceqb_rect_complete; intros.
   elim (@absurd_PCond_bottom l H0).
   split; trivial.
-    rewrite <- (morph0 CRmorph) in |- *; trivial.
+    rewrite <- (morph0 CRmorph); trivial.
  intros p H p0 H0 l1 H1.
    simpl in H1.
    case (H _ H1); intros H2 H3.
    case (H0 _ H3); intros H4 H5; split; auto.
-   simpl in |- *.
+   simpl.
    apply field_is_integral_domain; trivial.
- simpl in |- *; intros p H l1.
+ simpl; intros p H l1.
    apply ceqb_rect_complete; intros.
   elim (@absurd_PCond_bottom l H1).
   destruct (H _ H1).
@@ -1677,7 +1664,7 @@ Definition Fcons2 e l := Fcons1 (PExpr_simp e) l.
 
 Theorem PFcons2_fcons_inv:
  forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
-unfold Fcons2 in |- *; intros l a l1 H; split;
+unfold Fcons2; intros l a l1 H; split;
  case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto.
 intros H1 H2 H3; case H1.
 transitivity (NPEeval l a); trivial.
@@ -1756,50 +1743,48 @@ 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.
-   repeat rewrite (ARadd_assoc ARth) in |- *.
-   rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial.
+   repeat rewrite (ARadd_assoc ARth).
+   rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial.
 Qed.
 
 Lemma gen_phiPOS_inj : forall x y,
   gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
   x = y.
 intros x y.
-repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
+repeat rewrite <- (same_gen Rsth Reqe ARth).
 case (Pos.compare_spec x y).
  intros.
    trivial.
  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.
 
 
 Lemma gen_phiN_inj : forall x y,
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
   x = y.
-destruct x; destruct y; simpl in |- *; intros; trivial.
+destruct x; destruct y; simpl; intros; trivial.
  elim gen_phiPOS_not_0 with p.
-   symmetry  in |- *.
-   rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
+   symmetry .
+   rewrite (same_gen Rsth Reqe ARth); trivial.
  elim gen_phiPOS_not_0 with p.
-   rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
- rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial.
+   rewrite (same_gen Rsth Reqe ARth); trivial.
+ rewrite gen_phiPOS_inj with (1 := H); trivial.
 Qed.
 
 Lemma gen_phiN_complete : forall x y,
@@ -1824,17 +1809,17 @@ Section Field.
 Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
 intros.
 transitivity (x + (1 + - (1))).
- rewrite (Ropp_def Rth) in |- *.
-   symmetry  in |- *.
+ rewrite (Ropp_def Rth).
+   symmetry .
    apply (ARadd_0_r Rsth ARth).
  transitivity (y + (1 + - (1))).
-  repeat rewrite <- (ARplus_assoc ARth) in |- *.
-    repeat rewrite (ARadd_assoc ARth) in |- *.
+  repeat rewrite <- (ARplus_assoc ARth).
+    repeat rewrite (ARadd_assoc ARth).
     apply (Radd_ext Reqe).
-   repeat rewrite <- (ARadd_comm ARth 1) in |- *.
+   repeat rewrite <- (ARadd_comm ARth 1).
      trivial.
    reflexivity.
-  rewrite (Ropp_def Rth) in |- *.
+  rewrite (Ropp_def Rth).
     apply (ARadd_0_r Rsth ARth).
 Qed.
 
@@ -1846,14 +1831,14 @@ Let gen_phiPOS_inject :=
 
 Lemma gen_phiPOS_discr_sgn : forall x y,
   ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
-red in |- *; intros.
+red; intros.
 apply gen_phiPOS_not_0 with (y + x)%positive.
-rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+rewrite (ARgen_phiPOS_add Rsth Reqe ARth).
 transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
  apply (Radd_ext Reqe); trivial.
   reflexivity.
-  rewrite (same_gen Rsth Reqe ARth) in |- *.
-    rewrite (same_gen Rsth Reqe ARth) in |- *.
+  rewrite (same_gen Rsth Reqe ARth).
+    rewrite (same_gen Rsth Reqe ARth).
     trivial.
  apply (Ropp_def Rth).
 Qed.
@@ -1861,33 +1846,33 @@ Qed.
 Lemma gen_phiZ_inj : forall x y,
   gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
   x = y.
-destruct x; destruct y; simpl in |- *; intros.
+destruct x; destruct y; simpl; intros.
  trivial.
  elim gen_phiPOS_not_0 with p.
-   rewrite (same_gen Rsth Reqe ARth) in |- *.
-   symmetry  in |- *; trivial.
+   rewrite (same_gen Rsth Reqe ARth).
+   symmetry ; trivial.
  elim gen_phiPOS_not_0 with p.
-   rewrite (same_gen Rsth Reqe ARth) in |- *.
-   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
-   rewrite <- H in |- *.
+   rewrite (same_gen Rsth Reqe ARth).
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
+   rewrite <- H.
    apply (ARopp_zero Rsth Reqe ARth).
  elim gen_phiPOS_not_0 with p.
-   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   rewrite (same_gen Rsth Reqe ARth).
    trivial.
- rewrite gen_phiPOS_inject  with (1 := H) in |- *; trivial.
+ rewrite gen_phiPOS_inject  with (1 := H); trivial.
  elim gen_phiPOS_discr_sgn with (1 := H).
  elim gen_phiPOS_not_0 with p.
-   rewrite (same_gen Rsth Reqe ARth) in |- *.
-   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
-   rewrite H in |- *.
+   rewrite (same_gen Rsth Reqe ARth).
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
+   rewrite H.
    apply (ARopp_zero Rsth Reqe ARth).
  elim gen_phiPOS_discr_sgn with p0 p.
-   symmetry  in |- *; trivial.
+   symmetry ; trivial.
  replace p0 with p; trivial.
    apply gen_phiPOS_inject.
-   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
-   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *.
-   rewrite H in |- *; trivial.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)).
+   rewrite H; trivial.
    reflexivity.
 Qed.
 
@@ -1896,8 +1881,8 @@ Lemma gen_phiZ_complete : forall x y,
   Zeq_bool x y = true.
 intros.
  replace y with x.
- unfold Zeq_bool in |- *.
-   rewrite Zcompare_refl in |- *; trivial.
+ unfold Zeq_bool.
+   rewrite Z.compare_refl; trivial.
  apply gen_phiZ_inj; trivial.
 Qed.
 
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 763dbe7b..e805151c 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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).
@@ -396,14 +396,14 @@ Section NWORDMORPHISM.
 
  Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
 Proof.
-induction w; simpl in |- *; intros; auto.
+induction w; simpl; intros; auto.
  reflexivity.
 
  destruct a.
   destruct w.
    reflexivity.
 
-   rewrite IHw in |- *; trivial.
+   rewrite IHw; trivial.
    apply (ARopp_zero Rsth Reqe ARth).
 
    discriminate.
@@ -412,7 +412,7 @@ Qed.
   Lemma gen_phiNword_cons : forall w n,
     gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
 induction w.
- destruct n; simpl in |- *; norm.
+ destruct n; simpl; norm.
 
  intros.
  destruct n; norm.
@@ -423,27 +423,27 @@ Qed.
 destruct w; intros.
  destruct n; norm.
 
- unfold Nwcons in |- *.
- rewrite gen_phiNword_cons in |- *.
+ unfold Nwcons.
+ rewrite gen_phiNword_cons.
  reflexivity.
 Qed.
 
  Lemma gen_phiNword_ok : forall w1 w2,
    Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
 induction w1; intros.
- simpl in |- *.
- rewrite (gen_phiNword0_ok _ H) in |- *.
+ simpl.
+ rewrite (gen_phiNword0_ok _ H).
  reflexivity.
 
- rewrite gen_phiNword_cons in |- *.
+ rewrite gen_phiNword_cons.
  destruct w2.
   simpl in H.
   destruct a; try  discriminate.
-  rewrite (gen_phiNword0_ok _ H) in |- *.
+  rewrite (gen_phiNword0_ok _ H).
   norm.
 
   simpl in H.
-  rewrite gen_phiNword_cons in |- *.
+  rewrite gen_phiNword_cons.
   case_eq (N.eqb a n); intros H0.
    rewrite H0 in H.
    apply N.eqb_eq in H0. rewrite <- H0.
@@ -457,27 +457,27 @@ Qed.
 Lemma Nwadd_ok : forall x y,
    gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
 induction x; intros.
- simpl in |- *.
+ simpl.
  norm.
 
  destruct y.
   simpl Nwadd; norm.
 
-  simpl Nwadd in |- *.
-  repeat rewrite gen_phiNword_cons in |- *.
-  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by
+  simpl Nwadd.
+  repeat rewrite gen_phiNword_cons.
+  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by
     (destruct Reqe; constructor; trivial).
 
-  rewrite IHx in |- *.
+  rewrite IHx.
   norm.
   add_push (- gen_phiNword x); reflexivity.
 Qed.
 
 Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
-simpl in |- *.
-unfold Nwopp in |- *; simpl in |- *.
+simpl.
+unfold Nwopp; simpl.
 intros.
-rewrite gen_phiNword_Nwcons in |- *; norm.
+rewrite gen_phiNword_Nwcons; norm.
 Qed.
 
 Lemma Nwscal_ok : forall n x,
@@ -485,12 +485,12 @@ Lemma Nwscal_ok : forall n x,
 induction x; intros.
  norm.
 
- simpl Nwscal in |- *.
- repeat rewrite gen_phiNword_cons in |- *.
- rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *
+ simpl Nwscal.
+ repeat rewrite gen_phiNword_cons.
+ rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth))
    by (destruct Reqe; constructor; trivial).
 
-  rewrite IHx in |- *.
+  rewrite IHx.
   norm.
 Qed.
 
@@ -500,19 +500,19 @@ induction x; intros.
  norm.
 
  destruct a.
-  simpl Nwmul in |- *.
-  rewrite Nwopp_ok in |- *.
-  rewrite IHx in |- *.
-  rewrite gen_phiNword_cons in |- *.
+  simpl Nwmul.
+  rewrite Nwopp_ok.
+  rewrite IHx.
+  rewrite gen_phiNword_cons.
   norm.
 
-  simpl Nwmul in |- *.
-  unfold Nwsub in |- *.
-  rewrite Nwadd_ok in |- *.
-  rewrite Nwscal_ok in |- *.
-  rewrite Nwopp_ok in |- *.
-  rewrite IHx in |- *.
-  rewrite gen_phiNword_cons in |- *.
+  simpl Nwmul.
+  unfold Nwsub.
+  rewrite Nwadd_ok.
+  rewrite Nwscal_ok.
+  rewrite Nwopp_ok.
+  rewrite IHx.
+  rewrite gen_phiNword_cons.
   norm.
 Qed.
 
@@ -528,9 +528,9 @@ constructor.
  exact Nwadd_ok.
 
  intros.
- unfold Nwsub in |- *.
- rewrite Nwadd_ok in |- *.
- rewrite Nwopp_ok in |- *.
+ unfold Nwsub.
+ rewrite Nwadd_ok.
+ rewrite Nwopp_ok.
  norm.
 
  exact Nwmul_ok.
@@ -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 5a224e38..0c16fe1a 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/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index fafd16ab..fae98d83 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v
index 9a30fa47..7789ba3e 100644
--- a/plugins/setoid_ring/Ncring.v
+++ b/plugins/setoid_ring/Ncring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 3c79f7d9..528ad4f1 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 c0d31587..8e4b613f 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 34731eb3..44f8e7ff 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 56473adb..29372212 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -5,21 +5,21 @@ Require Import Rdefinitions.
 Require Import Rpow_def.
 Require Import Raxioms.
 
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
 Proof.
 constructor.
  intro; apply Rplus_0_l.
  exact Rplus_comm.
- symmetry  in |- *; apply Rplus_assoc.
+ symmetry ; apply Rplus_assoc.
  intro; apply Rmult_1_l.
  exact Rmult_comm.
- symmetry  in |- *; apply Rmult_assoc.
+ symmetry ; apply Rmult_assoc.
  intros m n p.
-   rewrite Rmult_comm in |- *.
-   rewrite (Rmult_comm n p) in |- *.
-   rewrite (Rmult_comm m p) in |- *.
+   rewrite Rmult_comm.
+   rewrite (Rmult_comm n p).
+   rewrite (Rmult_comm m p).
    apply Rmult_plus_distr_l.
  reflexivity.
  exact Rplus_opp_r.
@@ -42,17 +42,17 @@ destruct H0.
  apply Rlt_trans with (IZR (up x)); trivial.
     replace (IZR (up x)) with (x + (IZR (up x) - x))%R.
   apply Rplus_lt_compat_l; trivial.
-  unfold Rminus in |- *.
-    rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
-    rewrite <- Rplus_assoc in |- *.
-    rewrite Rplus_opp_r in |- *.
+  unfold Rminus.
+    rewrite (Rplus_comm (IZR (up x)) (- x)).
+    rewrite <- Rplus_assoc.
+    rewrite Rplus_opp_r.
     apply Rplus_0_l.
  elim H0.
-   unfold Rminus in |- *.
-   rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
-   rewrite <- Rplus_assoc in |- *.
-   rewrite Rplus_opp_r in |- *.
-   rewrite Rplus_0_l in |- *; trivial.
+   unfold Rminus.
+   rewrite (Rplus_comm (IZR (up x)) (- x)).
+   rewrite <- Rplus_assoc.
+   rewrite Rplus_opp_r.
+   rewrite Rplus_0_l; trivial.
 Qed.
 
 Notation Rset := (Eqsth R).
@@ -61,7 +61,7 @@ Notation Rext := (Eq_ext Rplus Rmult Ropp).
 Lemma Rlt_0_2 : 0 < 2.
 apply Rlt_trans with (0 + 1).
  apply Rlt_n_Sn.
- rewrite Rplus_comm in |- *.
+ rewrite Rplus_comm.
    apply Rplus_lt_compat_l.
     replace 1 with (0 + 1).
   apply Rlt_n_Sn.
@@ -69,19 +69,19 @@ apply Rlt_trans with (0 + 1).
 Qed.
 
 Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
-unfold Rgt in |- *.
-induction x; simpl in |- *; intros.
+unfold Rgt.
+induction x; simpl; intros.
  apply Rlt_trans with (1 + 0).
-  rewrite Rplus_comm in |- *.
+  rewrite Rplus_comm.
     apply Rlt_n_Sn.
   apply Rplus_lt_compat_l.
-    rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
-    rewrite Rmult_comm in |- *.
+    rewrite <- (Rmul_0_l Rset Rext RTheory 2).
+    rewrite Rmult_comm.
     apply Rmult_lt_compat_l.
    apply Rlt_0_2.
    trivial.
- rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
-   rewrite Rmult_comm in |- *.
+ rewrite <- (Rmul_0_l Rset Rext RTheory 2).
+   rewrite Rmult_comm.
    apply Rmult_lt_compat_l.
   apply Rlt_0_2.
   trivial.
@@ -93,9 +93,9 @@ Qed.
 
 Lemma Rgen_phiPOS_not_0 :
   forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.
-red in |- *; intros.
+red; intros.
 specialize (Rgen_phiPOS x).
-rewrite H in |- *; intro.
+rewrite H; intro.
 apply (Rlt_asym 0 0); trivial.
 Qed.
 
@@ -107,23 +107,23 @@ Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
 
 Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x  (n + m) = pow x n * pow x m.
 Proof.
-  intros x n; elim n; simpl in |- *; auto with real.
+  intros x n; elim n; simpl; auto with real.
   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.v b/plugins/setoid_ring/Ring.v
index c44c2edf..7c1bf981 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,7 +14,7 @@ Require Export Ring_tac.
 
 Lemma BoolTheory :
   ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
-split; simpl in |- *.
+split; simpl.
 destruct x; reflexivity.
 destruct x; destruct y; reflexivity.
 destruct x; destruct y; destruct z; reflexivity.
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index 6d4360d6..dc5248b2 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index b722a31b..b23ba352 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1,20 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 Set Implicit Arguments.
-Require Import Setoid.
-Require Import BinList.
-Require Import BinPos.
-Require Import BinNat.
-Require Import BinInt.
+Require Import Setoid Morphisms 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.
 
@@ -37,7 +33,7 @@ Section MakeRingPol.
  Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
                                 cO cI cadd cmul csub copp ceqb phi.
 
-  (* Power coefficients *)
+ (* Power coefficients *)
  Variable Cpow : Type.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.
@@ -50,26 +46,47 @@ Section MakeRingPol.
 
  (* R notations *)
  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).
+ Infix "+" := radd. Infix "*" := rmul.
+ Infix "-" := rsub. Notation "- x" := (ropp x).
+ Infix "==" := req.
+ Infix "^" := (pow_pos rmul).
 
  (* C notations *)
- 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).
+ Infix "+!" := cadd. Infix "*!" := cmul.
+ Infix "-! " := csub. Notation "-! x" := (copp x).
+ Infix "?=!" := ceqb. 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.
-  Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ 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.
+ Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
  Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
+
  Ltac add_push := gen_add_push radd Rsth Reqe ARth.
  Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
 
+ Ltac add_permut_rec t :=
+   match t with
+   | ?x + ?y => add_permut_rec y || add_permut_rec x
+   | _ => add_push t; apply (Radd_ext Reqe); [|reflexivity]
+   end.
+
+ Ltac add_permut :=
+  repeat (reflexivity ||
+    match goal with |- ?t == _ => add_permut_rec t end).
+
+ Ltac mul_permut_rec t :=
+   match t with
+   | ?x * ?y => mul_permut_rec y || mul_permut_rec x
+   | _ => mul_push t; apply (Rmul_ext Reqe); [|reflexivity]
+   end.
+
+ Ltac mul_permut :=
+  repeat (reflexivity ||
+    match goal with |- ?t == _ => mul_permut_rec t end).
+
+
  (* Definition of multivariable polynomials with coefficients in C :
     Type [Pol] represents [X1 ... Xn].
     The representation is Horner's where a [n] variable polynomial
@@ -116,19 +133,19 @@ Section MakeRingPol.
   | _, _ => false
   end.
 
- Notation " P ?== P' " := (Peq P P').
+ Infix "?==" := Peq.
 
  Definition mkPinj j P :=
   match P with
   | Pc _ => P
-  | Pinj j' Q => Pinj ((j + j'):positive) Q
+  | Pinj j' Q => Pinj (j + j') Q
   | _ => Pinj j P
   end.
 
  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.
 
@@ -156,14 +173,14 @@ Section MakeRingPol.
 
  (** Addition et subtraction *)
 
- Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol :=
+ Fixpoint PaddC (P:Pol) (c:C) : Pol :=
   match P with
   | Pc c1 => Pc (c1 +! c)
   | Pinj j Q => Pinj j (PaddC Q c)
   | PX P i Q => PX P i (PaddC Q c)
   end.
 
- Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol :=
+ Fixpoint PsubC (P:Pol) (c:C) : Pol :=
   match P with
   | Pc c1 => Pc (c1 -! c)
   | Pinj j Q => Pinj j (PsubC Q c)
@@ -175,11 +192,11 @@ Section MakeRingPol.
   Variable Pop : Pol -> Pol -> Pol.
   Variable Q : Pol.
 
-  Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol :=
+  Fixpoint PaddI (j:positive) (P:Pol) : Pol :=
    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,16 +204,16 @@ 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.
 
-  Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol :=
+  Fixpoint PsubI (j:positive) (P:Pol) : Pol :=
    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,41 +221,41 @@ 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.
 
  Variable P' : Pol.
 
- Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol :=
+ Fixpoint PaddX (i':positive) (P:Pol) : Pol :=
   match P with
   | Pc c => PX P' i' P
   | 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'
     end
   end.
 
- Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol :=
+ Fixpoint PsubX (i':positive) (P:Pol) : Pol :=
   match P with
   | Pc c => PX (--P') i' P
   | 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,18 +275,18 @@ 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')
       end
     end
   end.
- Notation "P ++ P'" := (Padd P P').
+ Infix "++" := Padd.
 
  Fixpoint Psub (P P': Pol) {struct P'} : Pol :=
   match P' with
@@ -281,22 +298,22 @@ 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')
       end
     end
   end.
- Notation "P -- P'" := (Psub P P').
+ Infix "--" := Psub.
 
  (** Multiplication *)
 
- Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol :=
+ Fixpoint PmulC_aux (P:Pol) (c:C) : Pol :=
   match P with
   | Pc c' => Pc (c' *! c)
   | Pinj j Q => mkPinj j (PmulC_aux Q c)
@@ -310,11 +327,11 @@ Section MakeRingPol.
  Section PmulI.
   Variable Pmul : Pol -> Pol -> Pol.
   Variable Q : Pol.
-  Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol :=
+  Fixpoint PmulI (j:positive) (P:Pol) : Pol :=
    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 +339,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 +357,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,25 +370,7 @@ 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').
+ Infix "**" := Pmul.
 
  Fixpoint Psquare (P:Pol) : Pol :=
    match P with
@@ -387,26 +385,26 @@ Section MakeRingPol.
 
  (** Monomial **)
 
+ (** A monomial is X1^k1...Xi^ki. Its representation
+     is a simplified version of the polynomial representation:
+
+     - [mon0] correspond to the polynom [P1].
+     - [(zmon j M)] corresponds to [(Pinj j ...)],
+       i.e. skip j variable indices.
+     - [(vmon i M)] is X^i*M with X the current variable,
+       its corresponds to (PX P1 i ...)]
+ *)
+
   Inductive Mon: Set :=
-    mon0: Mon
+  | mon0: Mon
   | zmon: positive -> Mon -> Mon
   | vmon: positive -> Mon -> Mon.
 
- Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R :=
-  match M with
-     mon0 => rI
-  | zmon j M1  => Mphi (jump j l) M1
-  | vmon i M1 =>
-     let x := hd 0 l in
-     let xi := pow_pos rmul x i in
-    (Mphi (tail l) M1) * xi
-  end.
-
  Definition mkZmon j M :=
    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
@@ -421,7 +419,7 @@ Section MakeRingPol.
    | Pinj j1 P1  =>
      let (R,S) := CFactor P1 c in
             (mkPinj j1 R, mkPinj j1 S)
-  | PX P1 i Q1 =>
+   | PX P1 i Q1 =>
      let (R1, S1) := CFactor P1 c in
      let (R2, S2) := CFactor Q1 c in
         (mkPX R1 i R2, mkPX S1 i S2)
@@ -429,10 +427,7 @@ Section MakeRingPol.
 
  Fixpoint MFactor (P: Pol) (c: C) (M: Mon) {struct P}: Pol * Pol :=
    match P, M with
-        _, mon0 =>
-            if (ceqb c cI) then (Pc cO, P) else
-(*            if (ceqb c (copp cI)) then (Pc cO, Popp P) else  Not in almost ring *)
-            CFactor P c
+        _, mon0 => if (ceqb c cI) then (Pc cO, P) else CFactor P c
    | Pc _, _    => (P, Pc cO)
    | Pinj j1 P1, zmon j2 M1 =>
       match j1 ?= j2 with
@@ -468,7 +463,7 @@ Section MakeRingPol.
     | _ => Some (Padd Q1 (Pmul P2 R1))
     end.
 
-  Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
+  Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) : Pol :=
     match POneSubst P1 cM1 P2 with
      Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end
     | _ => P1
@@ -480,14 +475,13 @@ Section MakeRingPol.
     | _ => None
     end.
 
-  Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}:
-     Pol :=
+  Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) : Pol :=
     match LM1 with
      cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
     | _ => P1
     end.
 
-  Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: option Pol :=
+  Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) : option Pol :=
     match LM1 with
      cons (M1,P2) LM2 =>
       match PNSubst P1 M1 P2 n with
@@ -497,7 +491,7 @@ Section MakeRingPol.
     | _ => None
     end.
 
-  Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol :=
+  Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) : Pol :=
     match PSubstL P1 LM1 n with
      Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
     | _ => P1
@@ -505,658 +499,409 @@ Section MakeRingPol.
 
  (** Evaluation of a polynomial towards R *)
 
- Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
+ Local Notation hd := (List.hd 0).
+
+ Fixpoint Pphi(l:list R) (P:Pol) : R :=
   match P with
   | Pc c => [c]
   | Pinj j Q => Pphi (jump j l) Q
-  | PX P i Q =>
-     let x := hd 0 l in
-     let xi := pow_pos rmul x i in
-    (Pphi l P) * xi + (Pphi (tail l) Q)
+  | PX P i Q => Pphi l P * (hd l) ^ i + Pphi (tail l) Q
   end.
 
  Reserved Notation "P @ l " (at level 10, no associativity).
  Notation "P @ l " := (Pphi l P).
+
+ (** Evaluation of a monomial towards R *)
+
+ Fixpoint Mphi(l:list R) (M: Mon) : R :=
+  match M with
+  | mon0 => rI
+  | zmon j M1 => Mphi (jump j l) M1
+  | vmon i M1 => Mphi (tail l) M1 * (hd l) ^ i
+  end.
+
+ Notation "M @@ l" := (Mphi l M) (at level 10, no associativity).
+
  (** 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 :=
+  match goal with |- context [Z.pos_sub ?x ?y] =>
+   generalize (Z.pos_sub_discr x y); destruct (Z.pos_sub x y)
   end.
+
+ Lemma jump_add' i j (l:list R) : jump (i + j) l = jump j (jump i l).
+ Proof. rewrite Pos.add_comm. apply jump_add. Qed.
+
+ Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l.
  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.
+  revert P';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 Peq_ok : forall P P',
-    (P ?== P') = true -> forall l, P@l == P'@ l.
+ Lemma Peq_spec P P' :
+   BoolSpec (forall l, P@l == P'@l) True (P ?== P').
  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.
+  generalize (Peq_ok P P'). destruct (P ?== P'); auto.
  Qed.
 
- Lemma Pphi0 : forall l, P0@l == 0.
+ Lemma Pphi0 l : P0@l == 0.
  Proof.
-  intros;simpl;apply (morph0 CRmorph).
+  simpl;apply (morph0 CRmorph).
  Qed.
 
- Lemma Pphi1 : forall l,  P1@l == 1.
+ Lemma Pphi1 l : P1@l == 1.
  Proof.
-  intros;simpl;apply (morph1 CRmorph).
+  simpl;apply (morph1 CRmorph).
  Qed.
 
- Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).
+ Lemma mkPinj_ok 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.
+  destruct P;simpl;rsimpl.
+  now rewrite jump_add'.
  Qed.
 
- Let pow_pos_Pplus :=
-    pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
+ Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
+ Proof.
+  rewrite Pos.add_comm.
+  apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
+ Qed.
 
- 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).
+ Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c').
  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.
+  generalize (morph_eq CRmorph c c').
+  destruct (c ?=! c'); auto.
  Qed.
 
- Ltac Esimpl :=
-  repeat (progress (
-   match goal with
-   | |- context [?P@?l] =>
-       match P with
-       | P0 => rewrite (Pphi0 l)
-       | P1 => rewrite (Pphi1 l)
-       | (mkPinj ?j ?P) => rewrite (mkPinj_ok j l P)
-       | (mkPX ?P ?i ?Q) => rewrite (mkPX_ok l P i Q)
-       end
-   | |- context [[?c]] =>
-       match c with
-       | cO => rewrite (morph0 CRmorph)
-       | cI => rewrite (morph1 CRmorph)
-       | ?x +! ?y => rewrite ((morph_add CRmorph) x y)
-       | ?x *! ?y => rewrite ((morph_mul CRmorph) x y)
-       | ?x -! ?y => rewrite ((morph_sub CRmorph) x y)
-       | -! ?x => rewrite ((morph_opp CRmorph) x)
-       end
-   end));
-  rsimpl; simpl.
-
- Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c].
+ Lemma mkPX_ok l P i Q :
+  (mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l).
  Proof.
-  induction P;simpl;intros;Esimpl;trivial.
-  rewrite IHP2;rsimpl.
+  unfold mkPX. destruct P.
+  - case ceqb_spec; intros H; simpl; try reflexivity.
+    rewrite H, (morph0 CRmorph), mkPinj_ok; rsimpl.
+  - reflexivity.
+  - case Peq_spec; intros H; simpl; try reflexivity.
+    rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl.
  Qed.
 
- Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c].
+ Hint Rewrite
+  Pphi0
+  Pphi1
+  mkPinj_ok
+  mkPX_ok
+  (morph0 CRmorph)
+  (morph1 CRmorph)
+  (morph0 CRmorph)
+  (morph_add CRmorph)
+  (morph_mul CRmorph)
+  (morph_sub CRmorph)
+  (morph_opp CRmorph)
+  : Esimpl.
+
+ (* Quicker than autorewrite with Esimpl :-) *)
+ Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl.
+
+ Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c].
  Proof.
-  induction P;simpl;intros.
-  Esimpl.
-  rewrite IHP;rsimpl.
+  revert l;induction P;simpl;intros;Esimpl;trivial.
   rewrite IHP2;rsimpl.
  Qed.
 
- Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c].
+ Lemma PsubC_ok c P l : (PsubC P c)@l == P@l - [c].
  Proof.
-  induction P;simpl;intros;Esimpl;trivial.
-  rewrite IHP1;rewrite IHP2;rsimpl.
-  mul_push ([c]);rrefl.
+  revert l;induction P;simpl;intros.
+  - Esimpl.
+  - rewrite IHP;rsimpl.
+  - rewrite IHP2;rsimpl.
  Qed.
 
- Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
+ Lemma PmulC_aux_ok c P l : (PmulC_aux 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.
-  assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
-  rewrite (H1 (refl_equal true));Esimpl.
-  apply PmulC_aux_ok.
+  revert l;induction P;simpl;intros;Esimpl;trivial.
+  rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut.
  Qed.
 
- Lemma Popp_ok : forall P l, (--P)@l == - P@l.
+ Lemma PmulC_ok c P l : (PmulC P c)@l == P@l * [c].
  Proof.
-  induction P;simpl;intros.
-  Esimpl.
-  apply IHP.
-  rewrite IHP1;rewrite IHP2;rsimpl.
+  unfold PmulC.
+  case ceqb_spec; intros H.
+  - rewrite H; Esimpl.
+  - case ceqb_spec; intros H'.
+    + rewrite H'; Esimpl.
+    + apply PmulC_aux_ok.
  Qed.
 
- Ltac Esimpl2 :=
-  Esimpl;
-  repeat (progress (
-   match goal with
-   | |- context [(PaddC ?P ?c)@?l] => rewrite (PaddC_ok c P l)
-   | |- context [(PsubC ?P ?c)@?l] => rewrite (PsubC_ok c P l)
-   | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l)
-   | |- context [(--?P)@?l] => rewrite (Popp_ok P l)
-   end)); Esimpl.
-
- Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l.
+ Lemma Popp_ok P l : (--P)@l == - P@l.
  Proof.
-  induction P';simpl;intros;Esimpl2.
-  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.
-  rewrite H;Esimpl. rewrite IHP';Esimpl.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
-  rewrite H;Esimpl. rewrite IHP.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
-  destruct p0;simpl.
-  rewrite IHP2;simpl;rsimpl.
-  rewrite IHP2;simpl.
-  rewrite jump_Pdouble_minus_one;rsimpl.
-  rewrite IHP';rsimpl.
-  destruct P;simpl.
-  Esimpl2;add_push [c];rrefl.
-  destruct p0;simpl;Esimpl2.
-  rewrite IHP'2;simpl.
-  rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));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.
-  rewrite IHP'1;rewrite IHP'2;rsimpl.
-  add_push (P3 @ (tail l));rewrite H;rrefl.
-  rewrite IHP'1;rewrite IHP'2;simpl;Esimpl.
-  rewrite H;rewrite Pplus_comm.
-  rewrite pow_pos_Pplus;rsimpl.
-  add_push (P3 @ (tail l));rrefl.
-  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 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 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.
+  revert l;induction P;simpl;intros.
+  - Esimpl.
+  - apply IHP.
+  - rewrite IHP1, IHP2;rsimpl.
  Qed.
 
- Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
+ Hint Rewrite PaddC_ok PsubC_ok PmulC_ok Popp_ok : Esimpl.
+
+ Lemma PaddX_ok P' P k l :
+  (forall P l, (P++P')@l == P@l + P'@l) ->
+  (PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k.
  Proof.
-  induction P';simpl;intros;Esimpl2;trivial.
-  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';rsimpl.
-  rewrite H;Esimpl. rewrite IHP';Esimpl.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
-  rewrite H;Esimpl. rewrite IHP.
-  rewrite <- jump_Pplus;rewrite Pplus_comm;rrefl.
-  destruct p0;simpl.
-  rewrite IHP2;simpl;rsimpl.
-  rewrite IHP2;simpl.
-  rewrite jump_Pdouble_minus_one;rsimpl.
-  rewrite IHP';rsimpl.
-  destruct P;simpl.
-  repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl.
-  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.
-  rewrite IHP'1; rewrite IHP'2;rsimpl.
-  add_push (P3 @ (tail l));rewrite H;rrefl.
-   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.
-  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.
-   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.
-  rewrite H0;rsimpl.
-  rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)).
-  rewrite H;rewrite Pplus_comm.
-  rewrite pow_pos_Pplus;rsimpl.
+  intros IHP'.
+  revert k l. induction P;simpl;intros.
+  - add_permut.
+  - destruct p; simpl;
+    rewrite ?jump_pred_double; add_permut.
+  - destr_pos_sub; intros ->;Esimpl.
+    + rewrite IHP';rsimpl. add_permut.
+    + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut.
+    + rewrite IHP1, pow_pos_add;rsimpl. add_permut.
  Qed.
-(* Proof for the symmetriv version *)
 
- Lemma PmulI_ok :
-  forall P',
-   (forall (P : Pol) (l : list R), (Pmul P P') @ l == P @ l * P' @ l) ->
-   forall (P : Pol) (p : positive) (l : list R),
-    (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
+ Lemma Padd_ok P' P l : (P ++ P')@l == P@l + 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.
+  revert P l; induction P';simpl;intros;Esimpl.
+  - revert p l; induction P;simpl;intros.
+    + Esimpl; add_permut.
+    + destr_pos_sub; intros ->;Esimpl.
+      * now rewrite IHP'.
+      * rewrite IHP';Esimpl. now rewrite jump_add'.
+      * rewrite IHP. now rewrite jump_add'.
+    + destruct p0;simpl.
+      * rewrite IHP2;simpl. rsimpl.
+      * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl.
+      * rewrite IHP'. rsimpl.
+  - destruct P;simpl.
+    + Esimpl. add_permut.
+    + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl.
+      * rsimpl. add_permut.
+      * rewrite jump_pred_double. rsimpl. add_permut.
+      * rsimpl. add_permut.
+    + destr_pos_sub; intros ->; Esimpl.
+      * rewrite IHP'1, IHP'2;rsimpl. add_permut.
+      * rewrite IHP'1, IHP'2;simpl;Esimpl.
+        rewrite pow_pos_add;rsimpl. add_permut.
+      * rewrite PaddX_ok by trivial; rsimpl.
+        rewrite IHP'2, pow_pos_add; rsimpl. add_permut.
  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).
+ Lemma PsubX_ok P' P k l :
+  (forall P l, (P--P')@l == P@l - P'@l) ->
+  (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k.
  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.
+  intros IHP'.
+  revert k l. induction P;simpl;intros.
+  - rewrite Popp_ok;rsimpl; add_permut.
+  - destruct p; simpl;
+    rewrite Popp_ok;rsimpl;
+    rewrite ?jump_pred_double; add_permut.
+  - destr_pos_sub; intros ->; Esimpl.
+    + rewrite IHP';rsimpl. add_permut.
+    + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut.
+    + rewrite IHP1, pow_pos_add;rsimpl. add_permut.
  Qed.
 
- Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux P P')@l == P@l * P'@l.
+ Lemma Psub_ok P' P l : (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.
+  revert P l; induction P';simpl;intros;Esimpl.
+  - revert p l; induction P;simpl;intros.
+    + Esimpl; add_permut.
+    + destr_pos_sub; intros ->;Esimpl.
+      * rewrite IHP';rsimpl.
+      * rewrite IHP';Esimpl. now rewrite jump_add'.
+      * rewrite IHP. now rewrite jump_add'.
+    + destruct p0;simpl.
+      * rewrite IHP2;simpl. rsimpl.
+      * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl.
+      * rewrite IHP'. rsimpl.
+  - destruct P;simpl.
+    + Esimpl; add_permut.
+    + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl.
+      * rsimpl. add_permut.
+      * rewrite jump_pred_double. rsimpl. add_permut.
+      * rsimpl. add_permut.
+    + destr_pos_sub; intros ->; Esimpl.
+      * rewrite IHP'1, IHP'2;rsimpl. add_permut.
+      * rewrite IHP'1, IHP'2;simpl;Esimpl.
+        rewrite pow_pos_add;rsimpl. add_permut.
+      * rewrite PsubX_ok by trivial;rsimpl.
+        rewrite IHP'2, pow_pos_add;rsimpl. add_permut.
  Qed.
-*)
 
-(* Proof for the symmetric version *)
- Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+ Lemma PmulI_ok P' :
+   (forall P l, (Pmul P P') @ l == P @ l * P' @ l) ->
+   forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
  Proof.
-  intros P P';generalize P;clear P;induction P';simpl;intros.
-  apply PmulC_ok. apply PmulI_ok;trivial.
-  destruct P.
-  rewrite (ARmul_comm ARth);Esimpl2;Esimpl2.
-  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
-           | 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 H;Esimpl.
-   rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2.
-   repeat (rewrite IHP'1 || rewrite IHP'2);simpl.
-   rewrite PmulI_ok;trivial.
-   mul_push (P'1@l). simpl. mul_push (P'2 @ (tail l)). Esimpl.
+  intros IHP'.
+  induction P;simpl;intros.
+  - Esimpl; mul_permut.
+  - destr_pos_sub; intros ->;Esimpl.
+    + now rewrite IHP'.
+    + now rewrite IHP', jump_add'.
+    + now rewrite IHP, jump_add'.
+  - destruct p0;Esimpl; rewrite ?IHP1, ?IHP2; rsimpl.
+    + f_equiv. mul_permut.
+    + rewrite jump_pred_double. f_equiv. mul_permut.
+    + rewrite IHP'. f_equiv. mul_permut.
  Qed.
 
-(*
-Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+ Lemma Pmul_ok 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.
+  revert P l;induction P';simpl;intros.
+  - apply PmulC_ok.
+  - apply PmulI_ok;trivial.
+  - destruct P.
+    + rewrite (ARmul_comm ARth). Esimpl.
+    + Esimpl. f_equiv. rewrite IHP'1; Esimpl.
+      destruct p0;rewrite IHP'2;Esimpl.
+      rewrite jump_pred_double; Esimpl.
+    + rewrite Padd_ok, !mkPX_ok, Padd_ok, !mkPX_ok,
+       !IHP'1, !IHP'2, PmulI_ok; trivial. simpl. Esimpl.
+      add_permut; f_equiv; mul_permut.
  Qed.
-*)
 
- Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
+ Lemma Psquare_ok 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.
+  revert l;induction P;simpl;intros;Esimpl.
+  - apply IHP.
+  - rewrite Padd_ok, Pmul_ok;Esimpl.
+    rewrite IHP1, IHP2.
+    mul_push ((hd l)^p). now mul_push (P2@l).
  Qed.
 
-
- Lemma mkZmon_ok: forall M j l,
-   Mphi l (mkZmon j M) == Mphi l (zmon j M).
- intros M j l; case M; simpl; intros; rsimpl.
+ Lemma mkZmon_ok M j l :
+   (mkZmon j M) @@ l == (zmon j M) @@ l.
+ Proof.
+ destruct M; simpl; rsimpl.
  Qed.
 
- Lemma zmon_pred_ok : forall M j l,
-    Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M).
+ Lemma zmon_pred_ok M j l :
+   (zmon_pred j M) @@ (tail l) == (zmon j M) @@ l.
  Proof.
-   destruct j; simpl;intros auto; rsimpl.
-   rewrite mkZmon_ok;rsimpl.
-   rewrite mkZmon_ok;simpl. rewrite jump_Pdouble_minus_one; rsimpl.
+   destruct j; simpl; rewrite ?mkZmon_ok; simpl; rsimpl.
+   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.
+ Lemma mkVmon_ok M i l :
+   (mkVmon i M)@@l == M@@l * (hd l)^i.
  Proof.
   destruct M;simpl;intros;rsimpl.
-   rewrite zmon_pred_ok;simpl;rsimpl.
-  rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl.
+  - rewrite zmon_pred_ok;simpl;rsimpl.
+  - rewrite pow_pos_add;rsimpl.
  Qed.
 
- Lemma Mcphi_ok: forall P c l,
-    let (Q,R) := CFactor P c in
-      P@l == Q@l + (phi c) * (R@l).
+ Ltac destr_factor := match goal with
+  | H : context [CFactor ?P _] |- context [CFactor ?P ?c] =>
+    destruct (CFactor P c); destr_factor; rewrite H; clear H
+  | H : context [MFactor ?P _ _] |- context [MFactor ?P ?c ?M] =>
+    specialize (H M); destruct (MFactor P c M); destr_factor; rewrite H; clear H
+  | _ => idtac
+ end.
+
+ Lemma Mcphi_ok P c l :
+   let (Q,R) := CFactor P c in
+     P@l == Q@l + [c] * R@l.
  Proof.
- intros P; elim P; simpl; auto; clear P.
-   intros c c1 l; generalize (div_th.(div_eucl_th) c c1); case cdiv.
-   intros q r H; rewrite H.
-   Esimpl.
-   rewrite (ARadd_comm ARth); rsimpl.
- intros i P Hrec c l.
-  generalize (Hrec c (jump i l)); case CFactor.
-  intros R1 S1; Esimpl; auto.
- intros Q1 Qrec i R1 Rrec c l.
-   generalize (Qrec c l); case CFactor; intros S1 S2 HS.
-   generalize (Rrec c (tail l)); case CFactor; intros S3 S4 HS1.
-   rewrite HS; rewrite HS1; Esimpl.
-   apply (Radd_ext Reqe); rsimpl.
-   repeat rewrite <- (ARadd_assoc ARth).
-   apply (Radd_ext Reqe); rsimpl.
-   rewrite (ARadd_comm ARth); rsimpl.
+ revert l.
+ induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl.
+ - assert (H := div_th.(div_eucl_th) c0 c).
+   destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
+ - destr_factor. Esimpl.
+ - destr_factor. Esimpl. add_permut.
  Qed.
 
- Lemma Mphi_ok: forall P (cM: C * Mon) l,
-    let (c,M) := cM in
-    let (Q,R) := MFactor P c M in
-      P@l == Q@l + (phi c) * (Mphi l M) * (R@l).
+ Lemma Mphi_ok P (cM: C * Mon) l :
+   let (c,M) := cM in
+   let (Q,R) := MFactor P c M in
+     P@l == Q@l + [c] * M@@l * R@l.
  Proof.
- intros P; elim P; simpl; auto; clear P.
-   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.
-    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.
-   Esimpl.
-   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.
-     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 (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));
-       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.
-     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 (Hrec1 (c,zmon j M1) l);
-     case (MFactor P2 c (zmon j M1)).
-     intros R1 S1 H1.
-     generalize (Hrec2 (c, zmon_pred j M1) (List.tail l));
-     case (MFactor Q2 c (zmon_pred j M1)); simpl.
-     intros R2 S2 H2; rewrite H1; rewrite H2.
-     repeat rewrite mkPX_ok; simpl.
-     rsimpl.
-     apply radd_ext; rsimpl.
-     rewrite (ARadd_comm ARth); rsimpl.
-     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).
-       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.
-       repeat (rewrite <-(ARadd_assoc ARth)).
-       apply radd_ext; rsimpl.
-       rewrite (ARadd_comm ARth); rsimpl.
-       apply radd_ext; rsimpl.
-       repeat (rewrite <-(ARmul_assoc ARth)).
-       rewrite mkZmon_ok.
-       apply rmul_ext; rsimpl.
-       repeat (rewrite <-(ARmul_assoc ARth)).
-       apply rmul_ext; rsimpl.
-       rewrite (ARmul_comm ARth); rsimpl.
-       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.
-       rewrite mkPX_ok; rsimpl.
-       repeat (rewrite <-(ARadd_assoc ARth)).
-       apply radd_ext; rsimpl.
-       rewrite (ARadd_comm ARth); rsimpl.
-       apply radd_ext; rsimpl.
-       repeat (rewrite <-(ARmul_assoc ARth)).
-       apply rmul_ext; rsimpl.
-       rewrite (ARmul_comm ARth); rsimpl.
-       apply rmul_ext; rsimpl.
-       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);
-             case (MFactor P2 c (mkZmon 1 M1));
-        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
-       rewrite H; rsimpl.
-       rewrite mkPX_ok; rsimpl.
-       repeat (rewrite <-(ARadd_assoc ARth)).
-       apply radd_ext; rsimpl.
-       rewrite (ARadd_comm ARth); rsimpl.
-       apply radd_ext; rsimpl.
-       rewrite mkZmon_ok.
-       repeat (rewrite <-(ARmul_assoc ARth)).
-       apply rmul_ext; rsimpl.
-       rewrite (ARmul_comm ARth); rsimpl.
-       rewrite mkPX_ok; simpl; rsimpl.
-       rewrite (morph0 CRmorph); rsimpl.
-       repeat (rewrite <-(ARmul_assoc ARth)).
-       rewrite (ARmul_comm ARth (Q3@l)); rsimpl.
-       apply rmul_ext; rsimpl.
-       rewrite (ARmul_comm ARth); rsimpl.
-       repeat (rewrite <- (ARmul_assoc ARth)).
-       apply rmul_ext; rsimpl.
-       rewrite <- pow_pos_Pplus.
-       rewrite (Pplus_minus _ _ He); rsimpl.
+ destruct cM as (c,M). revert M l.
+ induction P; destruct M; intros l; simpl; auto;
+ try (case ceqb_spec; intro He);
+  try (case Pos.compare_spec; intros He); rewrite ?He;
+   destr_factor; simpl; Esimpl.
+ - assert (H := div_th.(div_eucl_th) c0 c).
+   destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
+ - assert (H := Mcphi_ok P c). destr_factor. Esimpl.
+ - now rewrite <- jump_add, Pos.sub_add.
+ - assert (H2 := Mcphi_ok P2 c). assert (H3 := Mcphi_ok P3 c).
+   destr_factor. Esimpl. add_permut.
+ - rewrite zmon_pred_ok. simpl. add_permut.
+ - rewrite mkZmon_ok. simpl. add_permut. mul_permut.
+ - add_permut. mul_permut.
+   rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add by trivial; rsimpl.
+ - rewrite mkZmon_ok. simpl. Esimpl. add_permut. mul_permut.
+   rewrite <- pow_pos_add, 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.
+ Lemma POneSubst_ok P1 cM1 P2 P3 l :
+   POneSubst P1 cM1 P2 = Some P3 ->
+   [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == P3@l.
  Proof.
- intros P2 (cc,M1) P3 P4 l; unfold POneSubst.
- generalize (Mphi_ok P2 (cc, M1) l); case (MFactor P2 cc 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.
- (* new version *)
-   rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
- intros i P5 H; rewrite H.
-   intros HH H1; injection HH; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl.
- intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
-   assert (P4 = Q1 ++ P3 ** PX i P5 P6).
-   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.
+ destruct cM1 as (cc,M1).
+ unfold POneSubst.
+ assert (H := Mphi_ok P1 (cc, M1) l). simpl in H.
+ destruct MFactor as (R1,S1); simpl. rewrite H. clear H.
+ intros EQ EQ'. replace P3 with (R1 ++ P2 ** S1).
+ - rewrite EQ', Padd_ok, Pmul_ok; rsimpl.
+ - revert EQ. destruct S1; try now injection 1.
+   case ceqb_spec; now inversion 2.
  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.
+
+ Lemma PNSubst1_ok n P1 cM1 P2 l :
+   [fst cM1] * (snd cM1)@@l == P2@l ->
+   P1@l == (PNSubst1 P1 cM1 P2 n)@l.
  Proof.
- intros n; elim n; simpl; auto.
-   intros P2 M1 P3 l H.
-   generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
-   case (POneSubst P2 M1 P3); [idtac | intros; rsimpl].
-   intros P4 Hrec; rewrite (Hrec P4); auto; rsimpl.
- intros n1 Hrec P2 M1 P3 l H.
-   generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
-   case (POneSubst P2 M1 P3); [idtac | intros; rsimpl].
-   intros P4 Hrec1; rewrite (Hrec1 P4); auto; rsimpl.
+ revert P1. induction n; simpl; intros P1;
+ generalize (POneSubst_ok P1 cM1 P2); destruct POneSubst;
+   intros; rewrite <- ?IHn; auto; reflexivity.
  Qed.
 
- Lemma PNSubst_ok: forall n P1 M1 P2 l P3,
-    PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == P3@l.
+ Lemma PNSubst_ok n P1 cM1 P2 l P3 :
+   PNSubst P1 cM1 P2 n = Some P3 ->
+   [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == P3@l.
  Proof.
- intros n P2 (cc, M1) P3 l P4; unfold PNSubst.
- generalize (fun P4 => @POneSubst_ok P2 (cc,M1) P3 P4 l);
- case (POneSubst P2 (cc,M1) P3); [idtac | intros; discriminate].
- intros P5 H1; case n; try (intros; discriminate).
- intros n1 H2; injection H2; intros; subst.
- rewrite <- PNSubst1_ok; auto.
+ unfold PNSubst.
+ assert (H := POneSubst_ok P1 cM1 P2); destruct POneSubst; try discriminate.
+ destruct n; inversion_clear 1.
+ intros. rewrite <- PNSubst1_ok; auto.
  Qed.
 
- Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop :=
-    match LM1 with
-     cons (M1,P2) LM2 =>  ([fst M1] * Mphi l (snd M1) == P2@l) /\ (MPcond LM2 l)
-    | _ => True
-    end.
+ Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) : Prop :=
+   match LM1 with
+   | (M1,P2) :: LM2 => ([fst M1] * (snd M1)@@l == P2@l) /\ MPcond LM2 l
+   | _ => True
+   end.
 
- Lemma PSubstL1_ok: forall n LM1 P1 l,
-    MPcond LM1 l ->  P1@l == (PSubstL1 P1 LM1 n)@l.
+ Lemma PSubstL1_ok n LM1 P1 l :
+   MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l.
  Proof.
- intros n LM1; elim LM1; simpl; auto.
-   intros; rsimpl.
- intros (M2,P2) LM2 Hrec P3 l [H H1].
- rewrite <- Hrec; auto.
- apply PNSubst1_ok; auto.
+ revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros.
+ - reflexivity.
+ - rewrite <- IH by intuition. now apply PNSubst1_ok.
  Qed.
 
- Lemma PSubstL_ok: forall n LM1 P1 P2 l,
-   PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l ->  P1@l == P2@l.
+ Lemma PSubstL_ok n LM1 P1 P2 l :
+   PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l.
  Proof.
- intros n LM1; elim LM1; simpl; auto.
-   intros; discriminate.
- intros (M2,P2) LM2 Hrec P3 P4 l.
- generalize (PNSubst_ok n P3 M2 P2); case (PNSubst P3 M2 P2 n).
-   intros P5 H0 H1 [H2 H3]; injection H1; intros; subst.
-   rewrite <- PSubstL1_ok; auto.
- intros l1 H [H1 H2]; auto.
+ revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
+ - discriminate.
+ - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
+   * injection H; intros <-. rewrite <- PSubstL1_ok; intuition.
+   * now apply IH.
  Qed.
 
- Lemma PNSubstL_ok: forall m n LM1 P1 l,
-    MPcond LM1 l ->  P1@l == (PNSubstL P1 LM1 m n)@l.
+ Lemma PNSubstL_ok m n LM1 P1 l :
+    MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l.
  Proof.
- intros m; elim m; simpl; auto.
-   intros n LM1 P2 l H; generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l);
-     case (PSubstL P2 LM1 n); intros; rsimpl; auto.
- intros m1 Hrec n LM1 P2 l H.
- generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l);
-     case (PSubstL P2 LM1 n); intros; rsimpl; auto.
- rewrite <- Hrec; auto.
+ revert LM1 P1. induction m; simpl; intros;
+ assert (H' := PSubstL_ok n LM1 P2); destruct PSubstL;
+ auto; try reflexivity.
+ rewrite <- IHm; auto.
  Qed.
 
  (** Definition of polynomial expressions *)
@@ -1190,58 +935,22 @@ Strategy expand [PEeval].
 
  (** Correctness proofs *)
 
- Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
+ Lemma mkX_ok 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 <- nth_jump.
-  rewrite nth_Pdouble_minus_one;rrefl.
+  - now rewrite <-jump_tl, nth_jump.
+  - now rewrite <- nth_jump, nth_pred_double.
  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. *)
+ Hint Rewrite Padd_ok Psub_ok : Esimpl.
 
 Section POWER.
   Variable subst_l : Pol -> Pol.
-  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
+  Fixpoint Ppow_pos (res P:Pol) (p:positive) : Pol :=
    match p with
-   | xH => subst_l (Pmul res P)
+   | xH => subst_l (res ** P)
    | xO p => Ppow_pos (Ppow_pos res P p) P p
-   | xI p => subst_l (Pmul  (Ppow_pos (Ppow_pos res P p) P p) P)
+   | xI p => subst_l ((Ppow_pos (Ppow_pos res P p) P p) ** P)
    end.
 
   Definition Ppow_N P n :=
@@ -1250,17 +959,23 @@ Section POWER.
    | Npos p => Ppow_pos P1 P p
    end.
 
-  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
-         forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l.
+  Lemma Ppow_pos_ok l :
+    (forall P, subst_l P@l == P@l) ->
+    forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l.
   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.
+   intros subst_l_ok res P p. revert res.
+   induction p;simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp;
+    mul_permut.
   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.
+  Lemma Ppow_N_ok 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.
+  - reflexivity.
+  - rewrite Ppow_pos_ok by trivial. Esimpl.
+  Qed.
 
  End POWER.
 
@@ -1277,69 +992,66 @@ Section POWER.
    match pe with
    | PEc c => Pc c
    | PEX j => mk_X j
-   | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
-   | PEadd pe1 (PEopp pe2) =>
-     Psub (norm_aux pe1) (norm_aux pe2)
-   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
-   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
-   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
-   | PEopp pe1 => Popp (norm_aux pe1)
+   | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1)
+   | PEadd pe1 (PEopp pe2) => (norm_aux pe1) -- (norm_aux pe2)
+   | PEadd pe1 pe2 => (norm_aux pe1) ++ (norm_aux pe2)
+   | PEsub pe1 pe2 => (norm_aux pe1) -- (norm_aux pe2)
+   | PEmul pe1 pe2 => (norm_aux pe1) ** (norm_aux pe2)
+   | PEopp pe1 => -- (norm_aux pe1)
    | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
    end.
 
   Definition norm_subst pe := subst_l (norm_aux pe).
 
- (*
-  Fixpoint norm_subst (pe:PExpr) : Pol :=
+  (** Internally, [norm_aux] is expanded in a large number of cases.
+      To speed-up proofs, we use an alternative definition. *)
+
+  Definition get_PEopp pe :=
    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
+   | PEopp pe' => Some pe'
+   | _ => None
    end.
 
-  Lemma norm_subst_spec :
-     forall l pe, MPcond lmp l ->
-       PEeval l pe == (norm_subst pe)@l.
+  Lemma norm_aux_PEadd pe1 pe2 :
+    norm_aux (PEadd pe1 pe2) =
+    match get_PEopp pe1, get_PEopp pe2 with
+    | Some pe1', _ => (norm_aux pe2) -- (norm_aux pe1')
+    | None, Some pe2' => (norm_aux pe1) -- (norm_aux pe2')
+    | None, None => (norm_aux pe1) ++ (norm_aux pe2)
+    end.
   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.
+  simpl (norm_aux (PEadd _ _)).
+  destruct pe1; [ | | | | | reflexivity | ];
+   destruct pe2; simpl get_PEopp; reflexivity.
   Qed.
-*)
- Lemma norm_aux_spec :
-     forall l pe, MPcond lmp l ->
-       PEeval l pe == (norm_aux pe)@l.
+
+  Lemma norm_aux_PEopp pe :
+    match get_PEopp pe with
+    | Some pe' => norm_aux pe = -- (norm_aux pe')
+    | None => True
+    end.
+  Proof.
+  now destruct pe.
+  Qed.
+
+  Lemma norm_aux_spec l pe :
+    PEeval l pe == (norm_aux pe)@l.
   Proof.
    intros.
-   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 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.
+   induction pe.
+   - reflexivity.
+   - apply mkX_ok.
+   - simpl PEeval. rewrite IHpe1, IHpe2.
+     assert (H1 := norm_aux_PEopp pe1).
+     assert (H2 := norm_aux_PEopp pe2).
+     rewrite norm_aux_PEadd.
+     do 2 destruct get_PEopp; rewrite ?H1, ?H2; Esimpl; add_permut.
+   - simpl. rewrite IHpe1, IHpe2. Esimpl.
+   - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
+   - simpl. rewrite IHpe. Esimpl.
+   - simpl. rewrite Ppow_N_ok by reflexivity.
+     rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl.
+     induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok.
   Qed.
 
  Lemma norm_subst_spec :
@@ -1347,7 +1059,7 @@ Section POWER.
        PEeval l pe == (norm_subst pe)@l.
  Proof.
   intros;unfold norm_subst.
-  unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial.
+  unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec.
  Qed.
 
  End NORM_SUBST_REC.
@@ -1514,27 +1226,27 @@ Section POWER.
       (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R :=
    match P with
    | Pc c =>
-     let lm := add_pow_list (hd 0 fv) n lm in
+     let lm := add_pow_list (hd fv) n lm in
      mkadd_mult rP c lm
    | Pinj j Q =>
-     add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
+     add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 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)
+     else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd fv) n lm)
    end.
 
   Fixpoint mult_dev (P:Pol) (fv : list R) (n:N)
                      (lm:list (R*positive)) {struct P} : R :=
   (* P@l * (hd 0 l)^n * lm *)
   match P with
-  | 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)
+  | Pc c => mkmult_c c (add_pow_list (hd fv) n lm)
+  | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 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
+       let lmq := add_pow_list (hd fv) n lm in
        add_mult_dev rP Q (tail fv) N0 lmq
   end.
 
@@ -1575,7 +1287,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.
 
@@ -1617,11 +1329,11 @@ Qed.
  Qed.
 
  Lemma add_mult_dev_ok : forall P rP fv n lm,
-    add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm.
+    add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd fv) n * r_list_pow lm.
   Proof.
     induction P;simpl;intros.
-    rewrite mkadd_mult_ok. rewrite  add_pow_list_ok; Esimpl.
-    rewrite IHP. simpl. rewrite  add_pow_list_ok; Esimpl.
+    rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl.
+    rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl.
     change (match P3 with
        | Pc c => c ?=! cO
        | Pinj _ _ => false
@@ -1630,17 +1342,19 @@ 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  IHP2.
-   rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+    rewrite (H eq_refl).
+   rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
+   add_permut. mul_permut.
+   rewrite IHP2.
+   rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
+   add_permut. mul_permut.
  Qed.
 
  Lemma mult_dev_ok : forall P fv n lm,
-    mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm.
+    mult_dev P fv n lm == P@fv * pow_N rI rmul (hd fv) n * r_list_pow lm.
  Proof.
    induction P;simpl;intros;Esimpl.
    rewrite mkmult_c_ok;rewrite add_pow_list_ok;Esimpl.
@@ -1653,13 +1367,15 @@ 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).
+   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl.
+   mul_permut.
    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.
+   add_permut; mul_permut.
   Qed.
 
  Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P  == P@fv.
@@ -1676,18 +1392,18 @@ Qed.
    let mkmult_pow r x p := rmul r (mkpow x p) in
     Pphi_avoid mkpow mkopp_pow mkmult_pow.
 
- Lemma local_mkpow_ok :
-   forall (r : R) (p : positive),
+ Lemma local_mkpow_ok r p :
     match p with
     | xI _ => rpow r (Cp_phi (Npos p))
     | xO _ => rpow r (Cp_phi (Npos p))
     | 1 => r
     end == pow_pos rmul r p.
- Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. Qed.
+ Proof. destruct p; now rewrite ?pow_th.(rpow_pow_N). 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;
+   now rewrite ?local_mkpow_ok.
  Qed.
 
  Lemma ring_rw_pow_correct : forall n lH l,
@@ -1697,7 +1413,7 @@ Qed.
       PEeval l pe == Pphi_pow l npe.
  Proof.
   intros n lH l H1 lmp Heq1 pe npe Heq2.
-  rewrite Pphi_pow_ok. rewrite <- Heq2;rewrite <- Heq1.
+  rewrite Pphi_pow_ok, <- Heq2, <- Heq1.
   apply norm_subst_ok. trivial.
  Qed.
 
@@ -1711,58 +1427,48 @@ 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.
 
   Definition Pphi_dev := Pphi_avoid mkpow mkopp_pow mkmult_pow.
 
-  Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p.
+  Lemma mkmult_pow_ok p r x : mkmult_pow r x p == r * x^p.
   Proof.
-    induction p;intros;simpl;Esimpl.
-    repeat rewrite IHp;Esimpl.
-    repeat rewrite IHp;Esimpl.
+    revert r; induction p;intros;simpl;Esimpl;rewrite !IHp;Esimpl.
   Qed.
 
- Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p.
+ Lemma mkpow_ok p x : mkpow x p == x^p.
   Proof.
     destruct p;simpl;intros;Esimpl.
-    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.
-    simpl;Esimpl.
-    trivial.
+    - rewrite !mkmult_pow_ok;Esimpl.
+    - rewrite mkmult_pow_ok;Esimpl.
+      change x with (x^1) at 1.
+      now rewrite <- pow_pos_add, Pos.add_1_r, Pos.succ_pred_double.
   Qed.
 
-  Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p.
+  Lemma mkopp_pow_ok p x : mkopp_pow x p == - x^p.
   Proof.
     destruct p;simpl;intros;Esimpl.
-    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.
-    simpl;Esimpl.
-    trivial.
+    - rewrite !mkmult_pow_ok;Esimpl.
+    - rewrite mkmult_pow_ok;Esimpl.
+      change x with (x^1) at 1.
+      now rewrite <- pow_pos_add, Pos.add_1_r, Pos.succ_pred_double.
   Qed.
 
  Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv.
   Proof.
    unfold Pphi_dev;intros;apply Pphi_avoid_ok.
-   intros;apply mkpow_ok.
-   intros;apply mkopp_pow_ok.
-   intros;apply mkmult_pow_ok.
+   - intros;apply mkpow_ok.
+   - intros;apply mkopp_pow_ok.
+   - intros;apply mkmult_pow_ok.
   Qed.
 
  Lemma ring_rw_correct : forall n lH l,
@@ -1776,6 +1482,4 @@ Qed.
   apply norm_subst_ok. trivial.
  Qed.
 
-
 End MakeRingPol.
-
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index d33e9a82..7a7ffcfd 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 ab992552..42ce4edc 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       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 88904865..58a4d7ea 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 d3ed36ee..3c4f6b86 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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 *)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 9d61c06d..580e78f6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)