Imported Upstream version 8.4dfsgupstream/8.4dfsg

23 files changed, 711 insertions, 1112 deletions

diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v
index 3031fd22..fa780671 100644
--- a/plugins/micromega/CheckerMaker.v
+++ b/plugins/micromega/CheckerMaker.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/micromega/Env.v b/plugins/micromega/Env.v
index 5f6c60be..caec7800 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.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        *)
@@ -12,10 +12,9 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import ZArith.
-Require Import Coq.Arith.Max.
-Require Import List.
+Require Import BinInt List.
 Set Implicit Arguments.
+Local Open Scope positive_scope.
 
 Section S.
 
@@ -23,154 +22,78 @@ Section S.
 
   Definition Env := positive -> D.
 
-  Definition jump (j:positive) (e:Env) := fun x => e (Pplus x j).
+  Definition jump (j:positive) (e:Env) := fun x => e (x+j).
 
-  Definition nth (n:positive) (e : Env ) := e n.
+  Definition nth (n:positive) (e:Env) := e n.
 
-  Definition hd (x:D) (e: Env)  := nth xH e.
+  Definition hd (e:Env) := nth 1 e.
 
-  Definition tail (e: Env) := jump xH e.
+  Definition tail (e:Env) := jump 1 e.
 
-  Lemma psucc : forall p, (match p with
-                              | xI y' => xO (Psucc y')
-                              | xO y' => xI y'
-                              | 1%positive => 2%positive
-                            end) = (p+1)%positive.
+  Lemma jump_add i j l x : jump (i + j) l x = jump i (jump j l) x.
   Proof.
-    destruct p.
-    auto with zarith.
-    rewrite xI_succ_xO.
-    auto with zarith.
-    reflexivity.
+    unfold jump. f_equal. apply Pos.add_assoc.
   Qed.
 
-  Lemma jump_Pplus : forall i j l,
-    forall x, jump (i + j) l x = jump i (jump j l) x.
-  Proof.
-    unfold jump.
-    intros.
-    rewrite Pplus_assoc.
-    reflexivity.
-  Qed.
-
-  Lemma jump_simpl : forall p l,
-    forall x, jump p l x =
+  Lemma jump_simpl p l x :
+    jump p l x =
     match p with
       | xH => tail l x
       | xO p => jump p (jump p l) x
       | xI p  => jump p (jump p (tail l)) x
     end.
   Proof.
-    destruct p ; unfold tail ; intros ;  repeat rewrite <- jump_Pplus.
-    (* xI p = p + p + 1 *)
-    rewrite xI_succ_xO.
-    rewrite Pplus_diag.
-    rewrite <- Pplus_one_succ_r.
-    reflexivity.
-    (* xO p = p + p *)
-    rewrite Pplus_diag.
-    reflexivity.
-    reflexivity.
+    destruct p; unfold tail; rewrite <- ?jump_add; f_equal;
+    now rewrite Pos.add_diag.
   Qed.
 
-  Ltac jump_s :=
-    repeat
-      match goal with
-        | |- context [jump xH ?e] => rewrite (jump_simpl xH)
-        | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
-        | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
-      end.
-
-  Lemma jump_tl : forall j l, forall x, tail (jump j l) x = jump j (tail l) x.
+  Lemma jump_tl j l x : tail (jump j l) x = jump j (tail l) x.
   Proof.
-    unfold tail.
-    intros.
-    repeat rewrite <- jump_Pplus.
-    rewrite Pplus_comm.
-    reflexivity.
+    unfold tail. rewrite <- !jump_add. f_equal. apply Pos.add_comm.
   Qed.
 
-  Lemma jump_Psucc : forall j l,
-    forall x, (jump (Psucc j) l x) = (jump 1 (jump j l) x).
+  Lemma jump_succ j l x : jump (Pos.succ j) l x = jump 1 (jump j l) x.
   Proof.
-    intros.
-    rewrite <- jump_Pplus.
-    rewrite Pplus_one_succ_r.
-    rewrite Pplus_comm.
-    reflexivity.
+    rewrite <- jump_add. f_equal. symmetry. apply Pos.add_1_l.
   Qed.
 
-  Lemma jump_Pdouble_minus_one : forall i l,
-    forall x, (jump (Pdouble_minus_one i) (tail l)) x = (jump i (jump i l)) x.
+  Lemma jump_pred_double i l x :
+    jump (Pos.pred_double i) (tail l) x = jump i (jump i l) x.
   Proof.
-    unfold tail.
-    intros.
-    repeat rewrite <- jump_Pplus.
-    rewrite <- Pplus_one_succ_r.
-    rewrite Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_diag.
-    reflexivity.
+    unfold tail. rewrite <- !jump_add. f_equal.
+    now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag.
   Qed.
 
-  Lemma jump_x0_tail : forall p l, forall x, jump (xO p) (tail l) x = jump (xI p) l x.
-  Proof.
-    intros.
-    unfold jump.
-    unfold tail.
-    unfold jump.
-    rewrite <- Pplus_assoc.
-    simpl.
-    reflexivity.
-  Qed.
-
-  Lemma nth_spec : forall p l x,
+  Lemma nth_spec p l :
     nth p l =
     match p with
-      | xH => hd x l
+      | xH => hd l
       | xO p => nth p (jump p l)
       | xI p => nth p (jump p (tail l))
     end.
   Proof.
-    unfold nth.
-    destruct p.
-    intros.
-    unfold jump, tail.
-    unfold jump.
-    rewrite Pplus_diag.
-    rewrite xI_succ_xO.
-    simpl.
-    reflexivity.
-    unfold jump.
-    rewrite Pplus_diag.
-    reflexivity.
-    unfold hd.
-    unfold nth.
-    reflexivity.
+    unfold hd, nth, tail, jump.
+    destruct p; f_equal; now rewrite Pos.add_diag.
   Qed.
 
-
-  Lemma nth_jump : forall p l x, nth p (tail l) = hd x (jump p l).
+  Lemma nth_jump p l : nth p (tail l) = hd (jump p l).
   Proof.
-    unfold tail.
-    unfold hd.
-    unfold jump.
-    unfold nth.
-    intros.
-    rewrite Pplus_comm.
-    reflexivity.
+    unfold hd, nth, tail, jump. f_equal. apply Pos.add_comm.
   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 p l :
+    nth (Pos.pred_double p) (tail l) = nth p (jump p l).
   Proof.
-    intros.
-    unfold tail.
-    unfold nth, jump.
-    rewrite Pplus_diag.
-    rewrite <- Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_one_succ_r.
-    reflexivity.
+    unfold nth, tail, jump. f_equal.
+    now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag.
   Qed.
 
 End S.
 
+Ltac jump_simpl :=
+  repeat
+    match goal with
+      | |- appcontext [jump xH] => rewrite (jump_simpl xH)
+      | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p))
+      | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p))
+    end.
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 309ebdef..786c3393 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.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        *)
@@ -11,15 +11,10 @@
 
 
 Set Implicit Arguments.
-Require Import Setoid.
-Require Import BinList.
-Require Import Env.
-Require Import BinPos.
-Require Import BinNat.
-Require Import BinInt.
+Require Import Setoid Morphisms Env BinPos BinNat BinInt.
 Require Export Ring_theory.
 
-Open Local Scope positive_scope.
+Local Open Scope positive_scope.
 Import RingSyntax.
 
 Section MakeRingPol.
@@ -30,7 +25,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.
 
@@ -42,35 +37,55 @@ 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.
  Variable pow_th : power_theory rI rmul req Cp_phi rpow.
 
-
  (* 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).
-
- (* Usefull 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.
+ Infix "+!" := cadd. Infix "*!" := cmul.
+ Infix "-! " := csub. Notation "-! x" := (copp x).
+ Infix "?=!" := ceqb. Notation "[ x ]" := (phi x).
+
+ (* Useful tactics *)
+ 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
@@ -117,19 +132,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.
 
@@ -157,14 +172,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)
@@ -176,11 +191,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')
@@ -188,16 +203,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')
@@ -205,41 +220,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'
@@ -259,18 +274,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
@@ -282,22 +297,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)
@@ -311,11 +326,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')
@@ -323,13 +338,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
@@ -342,7 +356,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'
@@ -355,25 +369,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
@@ -388,26 +384,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:Env 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
@@ -416,7 +412,7 @@ Section MakeRingPol.
    | vmon i' m => vmon (i+i') m
    end.
 
- Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
+ Fixpoint MFactor (P: Pol) (M: Mon) : Pol * Pol :=
    match P, M with
         _, mon0 => (Pc cO, P)
    | Pc _, _    => (P, Pc cO)
@@ -453,7 +449,7 @@ Section MakeRingPol.
     | _ => Some (Padd Q1 (Pmul P2 R1))
     end.
 
-  Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
+  Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) : Pol :=
     match POneSubst P1 M1 P2 with
      Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end
     | _ => P1
@@ -465,14 +461,13 @@ Section MakeRingPol.
     | _ => None
     end.
 
-  Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}:
-     Pol :=
+  Fixpoint PSubstL1 (P1: Pol) (LM1: list (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 (Mon * Pol)) (n: nat) {struct LM1}: option Pol :=
+  Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) : option Pol :=
     match LM1 with
      cons (M1,P2) LM2 =>
       match PNSubst P1 M1 P2 n with
@@ -482,7 +477,7 @@ Section MakeRingPol.
     | _ => None
     end.
 
-  Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol :=
+  Fixpoint PNSubstL (P1: Pol) (LM1: list (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
@@ -490,726 +485,446 @@ Section MakeRingPol.
 
  (** Evaluation of a polynomial towards R *)
 
- Fixpoint Pphi(l:Env R) (P:Pol) {struct P} : R :=
+ Fixpoint Pphi(l:Env 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:Env 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 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 env_morph : forall p e1 e2, (forall x, e1 x = e2 x) ->
- p @ e1 = p @ e2.
+ Lemma Pphi1 l : P1@l == 1.
+ Proof.
+  simpl;apply (morph1 CRmorph).
+ Qed.
+
+Lemma env_morph p e1 e2 :
+  (forall x, e1 x = e2 x) -> p @ e1 = p @ e2.
 Proof.
-  induction p ; simpl.
-  reflexivity.
-  intros.
-  apply IHp.
-  intros.
-  unfold jump.
-  apply H.
-  intros.
-  rewrite (IHp1 e1 e2) ; auto.
-  rewrite (IHp2 (tail e1) (tail e2)) ; auto.
-  unfold hd. unfold nth.  rewrite H.  reflexivity.
-  unfold tail.  unfold jump. intros ; apply H.
+  revert e1 e2. induction p ; simpl.
+  - reflexivity.
+  - intros e1 e2 EQ. apply IHp. intros. apply EQ.
+  - intros e1 e2 EQ. f_equal; [f_equal|].
+    + now apply IHp1.
+    + f_equal. apply EQ.
+    + apply IHp2. intros; apply EQ.
 Qed.
 
-Lemma Pjump_Pplus : forall P i j l, P @ (jump (i + j) l ) = P @ (jump j (jump i l)).
+Lemma Pjump_add P i j l :
+  P @ (jump (i + j) l) = P @ (jump j (jump i l)).
 Proof.
-  intros. apply env_morph. intros. rewrite <- jump_Pplus.
-  rewrite Pplus_comm.
-  reflexivity.
+  apply env_morph. intros. rewrite <- jump_add. f_equal.
+  apply Pos.add_comm.
 Qed.
 
-Lemma Pjump_xO_tail : forall P p l,
+Lemma Pjump_xO_tail P p l :
   P @ (jump (xO p) (tail l)) = P @ (jump (xI p) l).
 Proof.
-  intros.
-  apply env_morph.
-  intros.
-  rewrite (@jump_simpl R (xI p)).
-  rewrite (@jump_simpl R (xO p)).
-  reflexivity.
+  apply env_morph. intros. now jump_simpl.
 Qed.
 
-Lemma Pjump_Pdouble_minus_one : forall P p l,
-  P @ (jump (Pdouble_minus_one p) (tail l)) = P @ (jump (xO p) l).
+Lemma Pjump_pred_double P p l :
+  P @ (jump (Pos.pred_double p) (tail l)) = P @ (jump (xO p) l).
 Proof.
-  intros.
-  apply env_morph.
-  intros.
-  rewrite jump_Pdouble_minus_one.
-  rewrite (@jump_simpl R (xO p)).
-  reflexivity.
+  apply env_morph. intros.
+  rewrite jump_pred_double. now jump_simpl.
 Qed.
 
-
-
- Lemma Pphi1 : forall l,  P1@l == 1.
+ Lemma mkPinj_ok j l P : (mkPinj j P)@l == P@(jump j l).
  Proof.
-  intros;simpl;apply (morph1 CRmorph).
+  destruct P;simpl;rsimpl.
+  now rewrite Pjump_add.
  Qed.
 
- Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).
+ Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
  Proof.
-  intros j l p;destruct p;simpl;rsimpl.
-  rewrite Pjump_Pplus.
-  reflexivity.
+  rewrite Pos.add_comm.
+  apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
  Qed.
 
- Let pow_pos_Pplus :=
-    pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
-
- Lemma mkPX_ok : forall l P i Q,
-  (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l).
+ 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 [P0@?l] => rewrite (Pphi0 l)
-   | |- context [P1@?l] => rewrite (Pphi1 l)
-   | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P)
-   | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q)
-   | |- context [[cO]] => rewrite (morph0 CRmorph)
-   | |- context [[cI]] => rewrite (morph1 CRmorph)
-   | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y)
-   | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y)
-   | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y)
-   | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x)
-   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 Pjump_Pplus. rrefl.
-  rewrite H;Esimpl. rewrite IHP.
-  rewrite Pjump_Pplus. rrefl.
-  destruct p0;simpl.
-  rewrite IHP2;simpl. rsimpl.
-  rewrite Pjump_xO_tail. Esimpl.
-  rewrite IHP2;simpl.
-  rewrite Pjump_Pdouble_minus_one.
-  rsimpl.
-  rewrite IHP'.
-  rsimpl.
-  destruct P;simpl.
-  Esimpl2;add_push [c];rrefl.
-  destruct p0;simpl;Esimpl2.
-  rewrite IHP'2;simpl.
-  rewrite Pjump_xO_tail.
-  rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
-  rewrite IHP'2;simpl.
-  rewrite Pjump_Pdouble_minus_one. rsimpl.
-  add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
-  rewrite IHP'2;rsimpl.
-  unfold tail.
-  add_push (P @ (jump 1 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 Pjump_xO_tail.
-   apply (ARadd_comm ARth).
-   rewrite Pjump_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 <- Pjump_Pplus;rewrite Pplus_comm;rrefl.
-  rewrite H;Esimpl. rewrite IHP.
-  rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl.
-  destruct p0;simpl.
-  rewrite IHP2;simpl; try   rewrite Pjump_xO_tail ; rsimpl.
-  rewrite IHP2;simpl.
-  rewrite Pjump_Pdouble_minus_one;rsimpl.
-  unfold tail ; 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.
-  rewrite Pjump_xO_tail.
-  add_push (P @ ((jump (xI p0) l)));rrefl.
-  rewrite IHP'2;simpl;rewrite Pjump_Pdouble_minus_one;rsimpl.
-  add_push (- (P'1 @ l * pow_pos  rmul (hd 0 l) p));rrefl.
-  unfold tail.
-  rewrite IHP'2;rsimpl;add_push (P @ (jump 1 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.
-   rewrite Pjump_xO_tail.
-   apply (ARadd_comm ARth);trivial.
-   rewrite Pjump_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 ?Pjump_xO_tail, ?Pjump_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 symmetric version *)
 
- Lemma PmulI_ok :
-  forall P',
-   (forall (P : Pol) (l : Env  R), (Pmul P P') @ l == P @ l * P' @ l) ->
-   forall (P : Pol) (p : positive) (l : Env 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 Pjump_Pplus;simpl;rrefl.
-  rewrite H1.
-  rewrite Pjump_Pplus;rewrite IHP;rrefl.
-  destruct p0;Esimpl2.
-  rewrite IHP1;rewrite IHP2;rsimpl.
-  rewrite Pjump_xO_tail.
-  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 Pjump_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 Pjump_add.
+      * rewrite IHP. now rewrite Pjump_add.
+    + destruct p0;simpl.
+      * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl.
+      * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl.
+      * rewrite IHP'. rsimpl.
+  - destruct P;simpl.
+    + Esimpl. add_permut.
+    + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl.
+      * rewrite Pjump_xO_tail. rsimpl. add_permut.
+      * rewrite Pjump_pred_double. rsimpl. add_permut.
+      * rsimpl. unfold tail. 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 ?Pjump_xO_tail, ?Pjump_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 Pjump_add.
+      * rewrite IHP. now rewrite Pjump_add.
+    + destruct p0;simpl.
+      * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl.
+      * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl.
+      * rewrite IHP'. rsimpl.
+  - destruct P;simpl.
+    + Esimpl; add_permut.
+    + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl.
+      * rewrite Pjump_xO_tail. rsimpl. add_permut.
+      * rewrite Pjump_pred_double. rsimpl. add_permut.
+      * rsimpl. unfold tail. 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;rewrite IHP'2;Esimpl.
-   rewrite Pjump_xO_tail. reflexivity.
-   rewrite Pjump_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.
-   unfold tail.
-   mul_push (P'1@l). simpl. mul_push (P'2 @ (jump 1 l)). Esimpl.
+  intros IHP'.
+  induction P;simpl;intros.
+  - Esimpl; mul_permut.
+  - destr_pos_sub; intros ->;Esimpl.
+    + now rewrite IHP'.
+    + now rewrite IHP', Pjump_add.
+    + now rewrite IHP, Pjump_add.
+  - destruct p0;Esimpl; rewrite ?IHP1, ?IHP2; rsimpl.
+    + rewrite Pjump_xO_tail. f_equiv. mul_permut.
+    + rewrite Pjump_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. rewrite IHP'1;Esimpl. f_equiv.
+      destruct p0;rewrite IHP'2;Esimpl.
+      * now rewrite Pjump_xO_tail.
+      * rewrite Pjump_pred_double; Esimpl.
+    + rewrite Padd_ok, !mkPX_ok, Padd_ok, !mkPX_ok,
+       !IHP'1, !IHP'2, PmulI_ok; trivial. simpl. Esimpl.
+      unfold tail.
+      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 Mphi_morph : forall P env env', (forall x, env x = env' x ) ->
-   Mphi env P = Mphi env' P.
+ Lemma Mphi_morph M e1 e2 :
+  (forall x, e1 x = e2 x) -> M @@ e1 = M @@ e2.
  Proof.
-   induction P ; simpl.
-   reflexivity.
-   intros.
-   apply IHP.
-   intros.
-   unfold jump.
-   apply H.
-   (**)
-   intros.
-   replace (Mphi (tail env) P) with (Mphi (tail env') P).
-   unfold hd. unfold nth.
-   rewrite H.
-   reflexivity.
-   apply IHP.
-   unfold tail,jump.
-   intros. symmetry. apply H.
+   revert e1 e2; induction M; simpl; intros e1 e2 EQ; trivial.
+   - apply IHM. intros; apply EQ.
+   - f_equal.
+     * apply IHM. intros; apply EQ.
+     * f_equal. apply EQ.
  Qed.
 
-Lemma Mjump_xO_tail : forall M p l,
-  Mphi  (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M.
+Lemma Mjump_xO_tail M p l :
+  M @@ (jump (xO p) (tail l)) = M @@ (jump (xI p) l).
 Proof.
-  intros.
-  apply Mphi_morph.
-  intros.
-  rewrite (@jump_simpl R (xI p)).
-  rewrite (@jump_simpl R (xO p)).
-  reflexivity.
+  apply Mphi_morph. intros. now jump_simpl.
 Qed.
 
-Lemma Mjump_Pdouble_minus_one : forall M p l,
-  Mphi (jump (Pdouble_minus_one p) (tail l)) M = Mphi (jump (xO p) l) M.
+Lemma Mjump_pred_double M p l :
+  M @@ (jump (Pos.pred_double p) (tail l)) = M @@ (jump (xO p) l).
 Proof.
-  intros.
-  apply Mphi_morph.
-  intros.
-  rewrite jump_Pdouble_minus_one.
-  rewrite (@jump_simpl R (xO p)).
-  reflexivity.
+  apply Mphi_morph. intros.
+  rewrite jump_pred_double. now jump_simpl.
 Qed.
 
-Lemma Mjump_Pplus : forall M i j l, Mphi (jump (i + j) l ) M = Mphi (jump j (jump i l)) M.
+Lemma Mjump_add M i j l :
+  M @@ (jump (i + j) l) = M @@ (jump j (jump i l)).
 Proof.
-  intros. apply Mphi_morph. intros. rewrite <- jump_Pplus.
-  rewrite Pplus_comm.
-  reflexivity.
+  apply Mphi_morph. intros. now rewrite <- jump_add, Pos.add_comm.
 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 l; rsimpl.
-   rewrite mkZmon_ok;rsimpl.
-   simpl.
-   rewrite Mjump_xO_tail.
-   reflexivity.
-   rewrite mkZmon_ok;simpl.
-   rewrite Mjump_Pdouble_minus_one; rsimpl.
+   destruct j; simpl; rewrite ?mkZmon_ok; simpl; rsimpl.
+   - now rewrite Mjump_xO_tail.
+   - rewrite Mjump_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.
 
+ Ltac destr_mfactor R S := match goal with
+  | H : context [MFactor ?P _] |- context [MFactor ?P ?M] =>
+    specialize (H M); destruct MFactor as (R,S)
+ end.
 
- Lemma Mphi_ok: forall P M l,
-    let (Q,R) := MFactor P M in
-      P@l == Q@l + (Mphi l M) * (R@l).
+ Lemma Mphi_ok P M l :
+   let (Q,R) := MFactor P M in
+     P@l == Q@l + M@@l * R@l.
  Proof.
- intros P; elim P; simpl; auto; clear P.
-   intros c M l; case M; simpl; auto; try intro p; try intro m;
-   try rewrite (morph0 CRmorph); rsimpl.
-
-   intros i P Hrec M l; case M; simpl; clear M.
-     rewrite (morph0 CRmorph); rsimpl.
-     intros j M.
-     case_eq (i ?= j); intros He; simpl.
-       rewrite (Pos.compare_eq _ _ He).
-       generalize (Hrec M (jump j l)); case (MFactor P M);
-        simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
-       generalize (Hrec (zmon (j -i) M) (jump i l));
-       case (MFactor P (zmon (j -i) M)); simpl.
-       intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
-       rewrite  <- (Pplus_minus _ _ (ZC2 _ _ He)).
-       rewrite Mjump_Pplus; auto.
-       rewrite (morph0 CRmorph); rsimpl.
-       intros P2 m; rewrite (morph0 CRmorph); rsimpl.
-
-   intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto.
-   rewrite (morph0 CRmorph); rsimpl.
-   intros j M1.
-     generalize (Hrec1 (zmon j M1) l);
-     case (MFactor P2 (zmon j M1)).
-     intros R1 S1 H1.
-     generalize (Hrec2 (zmon_pred j M1) (tail l));
-     case (MFactor Q2 (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 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1));
-        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
-       rewrite H; rewrite mkPX_ok; rsimpl.
-       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.
-       rewrite (ARmul_comm ARth); rsimpl.
-       generalize (Hrec1 (vmon (j - i) M1) l);
-             case (MFactor P2 (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 <- pow_pos_Pplus.
-       rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl.
-       generalize (Hrec1 (mkZmon 1 M1) l);
-             case (MFactor P2 (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 <- pow_pos_Pplus.
-       rewrite (Pplus_minus _ _ He); rsimpl.
+ revert M l; induction P; destruct M; intros l; simpl; auto; Esimpl.
+ - case Pos.compare_spec; intros He; simpl.
+   * destr_mfactor R1 S1. now rewrite IHP, He, !mkPinj_ok.
+   * destr_mfactor R1 S1. rewrite IHP; simpl.
+     now rewrite !mkPinj_ok, <- Mjump_add, Pos.add_comm, Pos.sub_add.
+   * Esimpl.
+ - destr_mfactor R1 S1. destr_mfactor R2 S2.
+   rewrite IHP1, IHP2, !mkPX_ok, zmon_pred_ok; simpl; rsimpl.
+   add_permut.
+ - case Pos.compare_spec; intros He; simpl; destr_mfactor R1 S1;
+   rewrite ?He, IHP1, mkPX_ok, ?mkZmon_ok; simpl; rsimpl;
+   unfold tail; add_permut; mul_permut.
+   * rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add by trivial; rsimpl.
+   * rewrite mkPX_ok. simpl. Esimpl. 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 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ Lemma POneSubst_ok P1 M1 P2 P3 l :
+   POneSubst P1 M1 P2 = Some P3 -> M1@@l == 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.
- (* 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.
+ unfold POneSubst.
+ assert (H := Mphi_ok P1). destr_mfactor R1 S1. 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,
-    Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
+
+ Lemma PNSubst1_ok n P1 M1 P2 l :
+    M1@@l == P2@l -> P1@l == (PNSubst1 P1 M1 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 M1 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 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ Lemma PNSubst_ok n P1 M1 P2 l P3 :
+    PNSubst P1 M1 P2 n = Some P3 -> M1@@l == P2@l -> P1@l == P3@l.
  Proof.
- intros n P2 M1 P3 l P4; unfold PNSubst.
- generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
- case (POneSubst P2 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 M1 P2); destruct POneSubst; try discriminate.
+ destruct n; inversion_clear 1.
+ intros. rewrite <- PNSubst1_ok; auto.
  Qed.
 
- Fixpoint MPcond (LM1: list (Mon * Pol)) (l: Env R) {struct LM1} : Prop :=
-    match LM1 with
-     cons (M1,P2) LM2 =>  (Mphi l M1 == P2@l) /\ (MPcond LM2 l)
-    | _ => True
-    end.
+ Fixpoint MPcond (LM1: list (Mon * Pol)) (l: Env R) : Prop :=
+   match LM1 with
+   | cons (M1,P2) LM2 => (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 *)
@@ -1228,7 +943,7 @@ Proof.
 
  (** evaluation of polynomial expressions towards R *)
 
- Fixpoint PEeval (l:Env R) (pe:PExpr) {struct pe} : R :=
+ Fixpoint PEeval (l:Env R) (pe:PExpr) : R :=
    match pe with
    | PEc c => phi c
    | PEX j => nth j l
@@ -1241,60 +956,23 @@ Proof.
 
  (** Correctness proofs *)
 
- Lemma mkX_ok : forall p l, nth  p l == (mk_X p) @ l.
+ Lemma mkX_ok p l : nth p l == (mk_X p) @ l.
  Proof.
   destruct p;simpl;intros;Esimpl;trivial.
   rewrite nth_spec ; auto.
   unfold hd.
-  rewrite <- nth_Pdouble_minus_one.
-  rewrite (nth_jump (Pdouble_minus_one p) l 1).
-  reflexivity.
+  now rewrite <- nth_pred_double, nth_jump.
  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 :=
@@ -1303,17 +981,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. trivial. Esimpl.  auto. 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.
 
@@ -1342,62 +1026,57 @@ Section POWER.
 
   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.
-   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 reflexivity.
-   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
-   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;rrefl.
+  now destruct pe.
   Qed.
 
+  Lemma norm_aux_spec l pe :
+    PEeval l pe == (norm_aux pe)@l.
+  Proof.
+   intros.
+   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.
 
  End NORM_SUBST_REC.
 
-
 End MakeRingPol.
-
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 19a98f87..64181cde 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.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        *)
@@ -51,7 +51,7 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 Extraction "micromega.ml"
   List.map simpl_cone (*map_cone  indexes*)
   denorm Qpower
-  n_of_Z N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+  n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 
 
 
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 97517957..b260feab 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.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/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 7f6cf79b..bcf84c6b 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.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        *)
@@ -81,14 +81,14 @@ Ltac lra :=
   first [ psatzl R | psatzl Q ].
 
 Ltac lia :=
-  zify ; unfold Zsucc in * ; 
-  (*cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ;*) xlia ; 
+  zify ; unfold Z.succ in * ;
+  (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ;
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
       apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
 
 Ltac nia :=
-  zify ; unfold Zsucc in * ; 
+  zify ; unfold Z.succ in * ;
   xnlia ;
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index f64504a5..792e2c3c 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.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        *)
@@ -60,7 +60,7 @@ Proof.
 Qed.
 
 
-(*Definition Zeval_expr :=  eval_pexpr 0 Zplus Zmult Zminus Zopp  (fun x => x) (fun x => Z_of_N x) (Zpower).*)
+(*Definition Zeval_expr :=  eval_pexpr 0 Z.add Z.mul Z.sub Z.opp  (fun x => x) (fun x => Z.of_N x) (Z.pow).*)
 Require Import EnvRing.
 
 Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
@@ -71,7 +71,7 @@ Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
     | PEopp pe1 => - (Qeval_expr env pe1)
-    | PEpow pe1 n => Qpower (Qeval_expr env pe1)  (Z_of_N n)
+    | PEpow pe1 n => Qpower (Qeval_expr env pe1)  (Z.of_N n)
   end.
 
 Lemma Qeval_expr_simpl : forall env e,
@@ -83,7 +83,7 @@ Lemma Qeval_expr_simpl : forall env e,
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
     | PEopp pe1 => - (Qeval_expr env pe1)
-    | PEpow pe1 n => Qpower (Qeval_expr env pe1)  (Z_of_N n)
+    | PEpow pe1 n => Qpower (Qeval_expr env pe1)  (Z.of_N n)
   end.
 Proof.
   destruct e ; reflexivity.
@@ -91,7 +91,7 @@ Qed.
 
 Definition Qeval_expr' := eval_pexpr  Qplus Qmult Qminus Qopp (fun x => x) (fun x => x) (pow_N 1 Qmult).
 
-Lemma QNpower : forall r n, r ^ Z_of_N n = pow_N 1 Qmult r n.
+Lemma QNpower : forall r n, r ^ Z.of_N n = pow_N 1 Qmult r n.
 Proof.
   destruct n ; reflexivity.
 Qed.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 2be99da1..d6f67485 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.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        *)
@@ -85,17 +85,17 @@ Qed.
 
 Ltac INR_nat_of_P :=
   match goal with
-    | H : context[INR (nat_of_P ?X)] |- _ => 
+    | H : context[INR (Pos.to_nat ?X)] |- _ =>
       revert H ; 
       let HH := fresh in
-        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (nat_of_P X))
-    | |- context[INR (nat_of_P ?X)] =>
+        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X))
+    | |- context[INR (Pos.to_nat ?X)] =>
       let HH := fresh in
-        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (nat_of_P X))
+        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X))
   end.
 
 Ltac add_eq expr val := set (temp := expr) ; 
-  generalize (refl_equal temp) ; 
+  generalize (eq_refl temp) ;
     unfold temp at 1 ; generalize temp ; intro val ; clear temp.
 
 Ltac Rinv_elim :=
@@ -210,7 +210,7 @@ Proof.
   rewrite plus_IZR in *.
   rewrite mult_IZR in *.
   simpl.  
-  rewrite nat_of_P_mult_morphism.
+  rewrite Pos2Nat.inj_mul.
   rewrite mult_INR.
   rewrite mult_IZR.
   simpl.
@@ -244,7 +244,7 @@ Proof.
   simpl.
   repeat rewrite mult_IZR.
   simpl.  
-  rewrite nat_of_P_mult_morphism.
+  rewrite Pos2Nat.inj_mul.
   rewrite mult_INR.
   repeat INR_nat_of_P.
   intros. field ; split ; apply Rlt_neq ; auto.
@@ -275,7 +275,7 @@ Proof.
   apply Rlt_neq ; auto.
   simpl in H.
   exfalso.
-  rewrite Pmult_comm  in H.
+  rewrite Pos.mul_comm  in H.
   compute in H.
   discriminate.
 Qed.
@@ -291,7 +291,7 @@ Proof.
   destruct x.
   unfold Qopp.
   simpl.
-  rewrite Zopp_involutive.
+  rewrite Z.opp_involutive.
   reflexivity.
 Qed.
 
@@ -348,7 +348,7 @@ Proof.
   intros.
   assert ( 0 > x \/ 0 < x)%Q.
    destruct x ; unfold Qlt, Qeq in * ; simpl in *.
-   rewrite Zmult_1_r in *.
+   rewrite Z.mul_1_r in *.
    destruct Qnum ; simpl in * ; intuition auto.
    right. reflexivity.
    left ; reflexivity.
@@ -379,7 +379,7 @@ Proof.
 Qed.
 
 
-Notation to_nat := N.to_nat. (*Nnat.nat_of_N*)
+Notation to_nat := N.to_nat.
 
 Lemma QSORaddon :
   @SORaddon R
@@ -471,7 +471,7 @@ Definition INZ (n:N) : R :=
     | Npos p => IZR (Zpos p)
   end.
 
-Definition Reval_expr := eval_pexpr  Rplus Rmult Rminus Ropp R_of_Rcst nat_of_N pow.
+Definition Reval_expr := eval_pexpr  Rplus Rmult Rminus Ropp R_of_Rcst N.to_nat pow.
 
 
 Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
@@ -490,10 +490,10 @@ Definition Reval_formula (e: PolEnv R) (ff : Formula Rcst) :=
 
 
 Definition Reval_formula' :=
-  eval_sformula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt nat_of_N pow R_of_Rcst.
+  eval_sformula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst.
 
 Definition QReval_formula := 
-  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR nat_of_N pow .
+  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR N.to_nat pow .
 
 Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
 Proof.
diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v
index b839195c..43bfb4d7 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 4af65086..fccacc74 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.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        *)
@@ -142,7 +142,7 @@ Qed.
 Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
 Definition PolEnv := Env R. (* For interpreting PolC *)
 Definition eval_pol (env : PolEnv) (p:PolC) : R :=
-   Pphi 0 rplus rtimes phi env p.
+   Pphi rplus rtimes phi env p.
 
 Inductive Op1 : Set := (* relations with 0 *)
 | Equal (* == 0 *)
@@ -320,7 +320,7 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C)
 
 Arguments map_option2 [A B C] f o o'.
 
-Definition Rops_wd := mk_reqe rplus rtimes ropp req
+Definition Rops_wd := mk_reqe (*rplus rtimes ropp req*)
                        sor.(SORplus_wd)
                        sor.(SORtimes_wd)
                        sor.(SORopp_wd).
@@ -469,17 +469,11 @@ Fixpoint ge_bool (n m  : nat) : bool :=
              end
    end.
 
-Lemma ge_bool_cases : forall n m, (if ge_bool n m then n >= m else n < m)%nat.
+Lemma ge_bool_cases : forall n m,
+ (if ge_bool n m then n >= m else n < m)%nat.
 Proof.
-  induction n ; simpl.
-  destruct m ; simpl.
-  constructor.
-  omega.
-  destruct m.
-  constructor.
-  omega.
-  generalize (IHn m).
-  destruct (ge_bool n m) ; omega.
+  induction n; destruct m ; simpl; auto with arith.
+  specialize (IHn m). destruct (ge_bool); auto with arith.
 Qed.
 
 
@@ -593,7 +587,7 @@ Definition paddC := PaddC cplus.
 Definition psubC := PsubC cminus.
 
 Definition PsubC_ok : forall c P env, eval_pol env (psubC  P c) == eval_pol env P - [c] :=
-  let Rops_wd := mk_reqe rplus rtimes ropp req
+  let Rops_wd := mk_reqe (*rplus rtimes ropp req*)
                        sor.(SORplus_wd)
                        sor.(SORtimes_wd)
                        sor.(SORopp_wd) in
@@ -601,7 +595,7 @@ Definition PsubC_ok : forall c P env, eval_pol env (psubC  P c) == eval_pol env
                 addon.(SORrm).
 
 Definition PaddC_ok : forall c P env, eval_pol env (paddC  P c) == eval_pol env P + [c] :=
-  let Rops_wd := mk_reqe rplus rtimes ropp req
+  let Rops_wd := mk_reqe (*rplus rtimes ropp req*)
                        sor.(SORplus_wd)
                        sor.(SORtimes_wd)
                        sor.(SORopp_wd) in
@@ -882,13 +876,14 @@ Qed.
 Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
   match p with
     | Pc c => PEc c
-    | Pinj j p => xdenorm  (Pplus j jmp ) p
+    | Pinj j p => xdenorm  (Pos.add j jmp ) p
     | PX p j q   => PEadd
       (PEmul (xdenorm jmp p) (PEpow (PEX _  jmp) (Npos j)))
-      (xdenorm (Psucc jmp) q)
+      (xdenorm (Pos.succ jmp) q)
   end.
 
-Lemma xdenorm_correct : forall p i  env, eval_pol (jump i env)  p == eval_pexpr env (xdenorm (Psucc i) p).
+Lemma xdenorm_correct : forall p i env,
+  eval_pol (jump i env) p == eval_pexpr env (xdenorm (Pos.succ i) p).
 Proof.
   unfold eval_pol.
   induction p.
@@ -896,22 +891,21 @@ Proof.
   (* Pinj *)
   simpl.
   intros.
-  rewrite Pplus_succ_permute_r.
+  rewrite Pos.add_succ_r.
   rewrite <- IHp.
   symmetry.
-  rewrite Pplus_comm.
-  rewrite Pjump_Pplus. reflexivity.
+  rewrite Pos.add_comm.
+  rewrite Pjump_add. reflexivity.
   (* PX *)
   simpl.
   intros.
-  rewrite <- IHp1.
-  rewrite <- IHp2.
+  rewrite <- IHp1, <- IHp2.
   unfold Env.tail , Env.hd.
-  rewrite <- Pjump_Pplus.
-  rewrite <- Pplus_one_succ_r.
+  rewrite <- Pjump_add.
+  rewrite Pos.add_1_r.
   unfold Env.nth.
   unfold jump at 2.
-  rewrite Pplus_one_succ_l.
+  rewrite <- Pos.add_1_l.
   rewrite addon.(SORpower).(rpow_pow_N).
   unfold pow_N. ring.
 Qed.
@@ -924,14 +918,14 @@ Proof.
   induction p.
   reflexivity.
   simpl.
-  rewrite <- Pplus_one_succ_r.
+  rewrite Pos.add_1_r.
   apply xdenorm_correct.
   simpl.
   intros.
   rewrite IHp1.
   unfold Env.tail.
   rewrite xdenorm_correct.
-  change (Psucc xH) with 2%positive.
+  change (Pos.succ xH) with 2%positive.
   rewrite addon.(SORpower).(rpow_pow_N).
   simpl. reflexivity.
 Qed.
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index b3ccdfcc..440070a1 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.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/micromega/VarMap.v b/plugins/micromega/VarMap.v
index f41252b7..9ff8044e 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 2bf3d8c3..e30295e6 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.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        *)
@@ -109,7 +109,7 @@ Qed.
 
 Lemma Zring_morph :
   ring_morph 0 1 rplus rtimes rminus ropp req
-             0%Z 1%Z Zplus Zmult Zminus Zopp
+             0%Z 1%Z Z.add Z.mul Z.sub Z.opp
              Zeq_bool gen_order_phi_Z.
 Proof.
 exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)).
@@ -122,7 +122,7 @@ try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_
 try apply (Rlt_0_1 sor); assumption.
 Qed.
 
-Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x.
+Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x.
 Proof.
 exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd
         (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))).
@@ -130,7 +130,7 @@ Qed.
 
 Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
 Proof.
-intros x y H. pattern y; apply Plt_ind with x.
+intros x y H. pattern y; apply Pos.lt_ind with x.
 rewrite phi_pos1_succ; apply (Rlt_succ_r sor).
 clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor).
 assumption.
@@ -150,9 +150,9 @@ apply -> (Ropp_lt_mono sor); apply clt_pos_morph.
 red. now rewrite Pos.compare_antisym.
 Qed.
 
-Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y].
+Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y].
 Proof.
-unfold Zle_bool; intros x y H.
+unfold Z.leb; intros x y H.
 case_eq (x ?= y)%Z; intro H1; rewrite H1 in H.
 le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1.
 le_less. now apply clt_morph.
@@ -162,9 +162,9 @@ Qed.
 Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y].
 Proof.
 intros x y H. unfold Zeq_bool in H.
-case_eq (Zcompare x y); intro H1; rewrite H1 in *; (discriminate || clear H).
+case_eq (Z.compare x y); intro H1; rewrite H1 in *; (discriminate || clear H).
 apply (Rlt_neq sor). now apply clt_morph.
-fold (x > y)%Z in H1. rewrite Zgt_iff_lt in H1.
+fold (x > y)%Z in H1. rewrite Z.gt_lt_iff in H1.
 apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph.
 Qed.
 
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 461f53b5..bdc4671d 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.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        *)
@@ -34,20 +34,20 @@ Require Import EnvRing.
 
 Open Scope Z_scope.
 
-Lemma Zsor : SOR 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt.
+Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt.
 Proof.
   constructor ; intros ; subst ; try (intuition (auto  with zarith)).
   apply Zsth.
   apply Zth.
-  destruct (Ztrichotomy n m) ; intuition (auto with zarith).
-  apply Zmult_lt_0_compat ; auto.
+  destruct (Z.lt_trichotomy n m) ; intuition.
+  apply Z.mul_pos_pos ; auto.
 Qed.
 
 Lemma ZSORaddon :
-  SORaddon 0 1 Zplus Zmult Zminus Zopp  (@eq Z) Zle (* ring elements *)
-  0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
-  Zeq_bool Zle_bool
-  (fun x => x) (fun x => x) (pow_N 1 Zmult).
+  SORaddon 0 1 Z.add Z.mul Z.sub Z.opp  (@eq Z) Z.le (* ring elements *)
+  0%Z 1%Z Z.add Z.mul Z.sub Z.opp (* coefficients *)
+  Zeq_bool Z.leb
+  (fun x => x) (fun x => x) (pow_N 1 Z.mul).
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
@@ -65,20 +65,20 @@ Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
     | PEX x => env x
     | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
     | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
-    | PEpow e1 n  => Zpower (Zeval_expr env e1) (Z_of_N n)
+    | PEpow e1 n  => Z.pow (Zeval_expr env e1) (Z.of_N n)
     | PEsub e1 e2 => (Zeval_expr env e1) - (Zeval_expr env e2)
-    | PEopp e   => Zopp (Zeval_expr env e)
+    | PEopp e   => Z.opp (Zeval_expr env e)
   end.
 
-Definition eval_expr := eval_pexpr  Zplus Zmult Zminus Zopp (fun x => x) (fun x => x) (pow_N 1 Zmult).
+Definition eval_expr := eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x => x) (pow_N 1 Z.mul).
 
-Lemma ZNpower : forall r n, r ^ Z_of_N n = pow_N 1 Zmult r n.
+Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n.
 Proof.
   destruct n.
   reflexivity.
   simpl.
-  unfold Zpower_pos.
-  replace (pow_pos Zmult r p) with (1 * (pow_pos Zmult r p)) by ring.
+  unfold Z.pow_pos.
+  replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring.
   generalize 1.
   induction p; simpl ; intros ; repeat rewrite IHp ; ring.
 Qed.
@@ -94,10 +94,10 @@ Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop :=
 match o with
 | OpEq =>  @eq Z
 | OpNEq => fun x y  => ~ x = y
-| OpLe => Zle
-| OpGe => Zge
-| OpLt => Zlt
-| OpGt => Zgt
+| OpLe => Z.le
+| OpGe => Z.ge
+| OpLt => Z.lt
+| OpGt => Z.gt
 end.
 
 Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
@@ -105,23 +105,23 @@ Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
     (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs).
 
 Definition Zeval_formula' :=
-  eval_formula  Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult).
+  eval_formula  Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul).
 
 Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f.
 Proof.
   destruct f ; simpl.
   rewrite Zeval_expr_compat. rewrite Zeval_expr_compat.
   unfold eval_expr.
-  generalize (eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
-        (fun x : N => x) (pow_N 1 Zmult) env Flhs).
-  generalize ((eval_pexpr Zplus Zmult Zminus Zopp (fun x : Z => x)
-        (fun x : N => x) (pow_N 1 Zmult) env Frhs)).
+  generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+        (fun x : N => x) (pow_N 1 Z.mul) env Flhs).
+  generalize ((eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+        (fun x : N => x) (pow_N 1 Z.mul) env Frhs)).
   destruct Fop ; simpl; intros ; intuition (auto with zarith).
 Qed.
 
 
 Definition eval_nformula :=
-  eval_nformula 0 Zplus Zmult  (@eq Z) Zle Zlt (fun x => x) .
+  eval_nformula 0 Z.add Z.mul  (@eq Z) Z.le Z.lt (fun x => x) .
 
 Definition Zeval_op1 (o : Op1) : Z -> Prop :=
 match o with
@@ -140,7 +140,7 @@ Qed.
 
 Definition ZWitness := Psatz Z.
 
-Definition ZWeakChecker := check_normalised_formulas 0 1 Zplus Zmult Zeq_bool Zle_bool.
+Definition ZWeakChecker := check_normalised_formulas 0 1 Z.add Z.mul Zeq_bool Z.leb.
 
 Lemma ZWeakChecker_sound :   forall (l : list (NFormula Z)) (cm : ZWitness),
   ZWeakChecker l cm = true ->
@@ -154,13 +154,13 @@ Proof.
   exact H.
 Qed.
 
-Definition psub  := psub Z0  Zplus Zminus Zopp Zeq_bool.
+Definition psub  := psub Z0  Z.add Z.sub Z.opp Zeq_bool.
 
-Definition padd  := padd Z0  Zplus Zeq_bool.
+Definition padd  := padd Z0  Z.add Zeq_bool.
 
-Definition norm  := norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool.
+Definition norm  := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool.
 
-Definition eval_pol := eval_pol 0  Zplus Zmult (fun x => x).
+Definition eval_pol := eval_pol Z.add Z.mul (fun x => x).
 
 Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub  lhs rhs) = eval_pol env lhs - eval_pol env rhs.
 Proof.
@@ -211,10 +211,10 @@ Proof.
       repeat rewrite eval_pol_add;
       repeat rewrite <- eval_pol_norm ; simpl in *;
   unfold eval_expr;
-  generalize (   eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : N => x) (pow_N 1 Zmult) env lhs);
-  generalize (eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
+  generalize (   eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+    (fun x : N => x) (pow_N 1 Z.mul) env lhs);
+  generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+    (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst;
     intuition (auto with zarith).
   Transparent padd.
 Qed.
@@ -248,17 +248,17 @@ Proof.
       repeat rewrite eval_pol_add;
       repeat rewrite <- eval_pol_norm ; simpl in *;
   unfold eval_expr;
-  generalize (   eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : N => x) (pow_N 1 Zmult) env lhs);
-  generalize (eval_pexpr  Zplus Zmult Zminus Zopp (fun x : Z => x)
-    (fun x : N => x) (pow_N 1 Zmult) env rhs) ; intros z1 z2 ; intros ; subst;
+  generalize (   eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+    (fun x : N => x) (pow_N 1 Z.mul) env lhs);
+  generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
+    (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst;
     intuition (auto with zarith).
   Transparent padd.
 Qed.
 
-Definition Zunsat := check_inconsistent 0  Zeq_bool Zle_bool.
+Definition Zunsat := check_inconsistent 0  Zeq_bool Z.leb.
 
-Definition Zdeduce := nformula_plus_nformula 0 Zplus Zeq_bool.
+Definition Zdeduce := nformula_plus_nformula 0 Z.add Zeq_bool.
 
 
 Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
@@ -270,7 +270,7 @@ Require Import Zdiv.
 Open Scope Z_scope.
 
 Definition ceiling (a b:Z) : Z :=
-  let (q,r) := Zdiv_eucl a b in
+  let (q,r) := Z.div_eucl a b in
     match r with
       | Z0 => q
       | _  => q + 1
@@ -279,47 +279,38 @@ Definition ceiling (a b:Z) : Z :=
 
 Require Import Znumtheory.
 
-Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Zdiv a b.
+Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b.
 Proof.
   unfold ceiling.
   intros.
   apply Zdivide_mod in H.
-  case_eq (Zdiv_eucl a b).
+  case_eq (Z.div_eucl a b).
   intros.
   change z with (fst (z,z0)).
   rewrite <- H0.
-  change (fst (Zdiv_eucl a b)) with (Zdiv a b).
+  change (fst (Z.div_eucl a b)) with (Z.div a b).
   change z0 with (snd (z,z0)).
   rewrite <- H0.
-  change (snd (Zdiv_eucl a b)) with (Zmod a b).
+  change (snd (Z.div_eucl a b)) with (Z.modulo a b).
   rewrite H.
   reflexivity.
 Qed.
 
-Lemma narrow_interval_lower_bound : forall a b x, a > 0 -> a * x  >= b -> x >= ceiling b a.
+Lemma narrow_interval_lower_bound a b x :
+  a > 0 -> a * x  >= b -> x >= ceiling b a.
 Proof.
+  rewrite !Z.ge_le_iff.
   unfold ceiling.
-  intros.
-  generalize (Z_div_mod b a H).
-  destruct (Zdiv_eucl b a).
-  intros.
-  destruct H1.
-  destruct H2.
-  subst.
-  destruct (Ztrichotomy z0 0) as [ HH1 | [HH2 | HH3]]; destruct z0 ; try auto with zarith ; try discriminate.
-  assert (HH :x >= z \/ x < z) by (destruct (Ztrichotomy x z) ; auto with zarith).
-  destruct HH ;auto.
-  generalize (Zmult_lt_compat_l _ _ _ H3 H1).
-  auto with zarith.
-  clear H2.
-  assert (HH :x >= z +1 \/ x <= z) by (destruct (Ztrichotomy x z) ; intuition (auto with zarith)).
-  destruct HH ;auto.
-  assert (0 < a) by auto with zarith.
-  generalize (Zmult_lt_0_le_compat_r _ _ _ H2 H1).
-  intros.
-  rewrite Zmult_comm  in H4.
-  rewrite (Zmult_comm z)  in H4.
-  auto with zarith.
+  intros Ha H.
+  generalize (Z_div_mod b a Ha).
+  destruct (Z.div_eucl b a) as (q,r). intros (->,(H1,H2)).
+  destruct r as [|r|r].
+  - rewrite Z.add_0_r in H.
+    apply Z.mul_le_mono_pos_l in H; auto with zarith.
+  - assert (0 < Z.pos r) by easy.
+    rewrite Z.add_1_r, Z.le_succ_l.
+    apply Z.mul_lt_mono_pos_l with a; auto with zarith.
+  - now elim H1.
 Qed.
 
 (** NB: narrow_interval_upper_bound is Zdiv.Zdiv_le_lower_bound *)
@@ -360,7 +351,7 @@ Proof.
   destruct x ; simpl ; intuition congruence.
 Qed.
 
-Definition ZgcdM (x y : Z) := Zmax (Zgcd x y) 1.
+Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1.
 
 
 Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) :=
@@ -378,7 +369,7 @@ Fixpoint Zgcd_pol (p : PolC Z) : (Z * Z) :=
 
 Fixpoint Zdiv_pol (p:PolC Z) (x:Z) : PolC Z :=
   match p with
-    | Pc c => Pc (Zdiv c x)
+    | Pc c => Pc (Z.div c x)
     | Pinj j p => Pinj j (Zdiv_pol p x)
     | PX p j q => PX (Zdiv_pol p x) j (Zdiv_pol q x)
   end.
@@ -421,10 +412,10 @@ Proof.
   intros.
   simpl.
   unfold ZgcdM.
-  generalize (Zgcd_is_pos z1 z2).
-  generalize (Zmax_spec (Zgcd z1 z2) 1).
-  generalize (Zgcd_is_pos (Zmax (Zgcd z1 z2) 1) z).
-  generalize (Zmax_spec (Zgcd (Zmax (Zgcd z1 z2) 1) z) 1).
+  generalize (Z.gcd_nonneg z1 z2).
+  generalize (Zmax_spec (Z.gcd z1 z2) 1).
+  generalize (Z.gcd_nonneg (Z.max (Z.gcd z1 z2) 1) z).
+  generalize (Zmax_spec (Z.gcd (Z.max (Z.gcd z1 z2) 1) z) 1).
   auto with zarith.
 Qed.
 
@@ -433,7 +424,7 @@ Proof.
   intros.
   induction H.
   constructor.
-  apply Zdivide_trans with (1:= H0) ; assumption.
+  apply Z.divide_trans with (1:= H0) ; assumption.
   constructor. auto.
   constructor ; auto.
 Qed.
@@ -444,20 +435,20 @@ Proof.
   exists c. ring.
 Qed.
 
-Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Zgcd a b | c).
+Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Z.gcd a b | c).
 Proof.
   intros a b c (q,Hq).
   destruct (Zgcd_is_gcd a b) as [(a',Ha) (b',Hb) _].
-  set (g:=Zgcd a b) in *; clearbody g.
+  set (g:=Z.gcd a b) in *; clearbody g.
   exists (q * a' + b').
-  symmetry in Hq. rewrite <- Zeq_plus_swap in Hq.
+  symmetry in Hq. rewrite <- Z.add_move_r in Hq.
   rewrite <- Hq, Hb, Ha. ring.
 Qed.
 
 Lemma Zdivide_pol_sub : forall p a b,
-  0 < Zgcd a b ->
-  Zdivide_pol a (PsubC Zminus p b) ->
-   Zdivide_pol (Zgcd a b) p.
+  0 < Z.gcd a b ->
+  Zdivide_pol a (PsubC Z.sub p b) ->
+   Zdivide_pol (Z.gcd a b) p.
 Proof.
   induction p.
   simpl.
@@ -477,7 +468,7 @@ Proof.
 Qed.
 
 Lemma Zdivide_pol_sub_0 : forall p a,
-  Zdivide_pol a (PsubC Zminus p 0) ->
+  Zdivide_pol a (PsubC Z.sub p 0) ->
    Zdivide_pol a p.
 Proof.
   induction p.
@@ -496,7 +487,7 @@ Qed.
 
 
 Lemma Zgcd_pol_div : forall p g c,
-  Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Zminus p c).
+  Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c).
 Proof.
   induction p ; simpl.
   (* Pc *)
@@ -511,12 +502,12 @@ Proof.
   case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros.
   inv H1.
   unfold ZgcdM at 1.
-  destruct (Zmax_spec (Zgcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1];
+  destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1];
   destruct HH1 as [HH1 HH1'] ; rewrite HH1'.
   constructor.
   apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2).
   unfold ZgcdM.
-  destruct (Zmax_spec  (Zgcd z1 z2)  1) as [HH2 | HH2].
+  destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
   destruct HH2.
   rewrite H2.
   apply Zdivide_pol_sub ; auto.
@@ -524,9 +515,9 @@ Proof.
   destruct HH2. rewrite H2.
   apply Zdivide_pol_one.
   unfold ZgcdM in HH1. unfold ZgcdM.
-  destruct (Zmax_spec  (Zgcd z1 z2)  1) as [HH2 | HH2].
+  destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
   destruct HH2. rewrite H2 in *.
-  destruct (Zgcd_is_gcd (Zgcd z1 z2) z); auto.
+  destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto.
   destruct HH2. rewrite H2.
   destruct (Zgcd_is_gcd 1  z); auto.
   apply Zdivide_pol_Zdivide with (x:= z).
@@ -539,7 +530,7 @@ Qed.
 
 
 
-Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Zminus p c) g))  + c.
+Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Z.sub p c) g))  + c.
 Proof.
   intros.
   rewrite <- Zdiv_pol_correct ; auto.
@@ -553,8 +544,8 @@ Qed.
 
 Definition makeCuttingPlane (p : PolC Z) : PolC  Z * Z :=
   let (g,c) := Zgcd_pol p in
-    if Zgt_bool g Z0
-      then (Zdiv_pol (PsubC Zminus p c) g , Zopp (ceiling (Zopp c) g))
+    if Z.gtb g Z0
+      then (Zdiv_pol (PsubC Z.sub p c) g , Z.opp (ceiling (Z.opp c) g))
       else (p,Z0).
 
 
@@ -562,13 +553,13 @@ Definition genCuttingPlane (f : NFormula Z) : option (PolC Z * Z * Op1) :=
   let (e,op) := f in
     match op with
       | Equal => let (g,c) := Zgcd_pol e in
-        if andb (Zgt_bool g Z0) (andb (negb (Zeq_bool c Z0)) (negb (Zeq_bool (Zgcd g c) g)))
+        if andb (Z.gtb g Z0) (andb (negb (Zeq_bool c Z0)) (negb (Zeq_bool (Z.gcd g c) g)))
           then None (* inconsistent *)
           else (* Could be optimised Zgcd_pol is recomputed *)
             let (p,c) := makeCuttingPlane e  in
               Some (p,c,Equal)
       | NonEqual => Some (e,Z0,op)
-      | Strict   =>  let (p,c) := makeCuttingPlane (PsubC Zminus e 1) in
+      | Strict   =>  let (p,c) := makeCuttingPlane (PsubC Z.sub e 1) in
         Some (p,c,NonStrict)
       | NonStrict => let (p,c) := makeCuttingPlane e  in
         Some (p,c,NonStrict)
@@ -595,7 +586,7 @@ Qed.
 
 
 Definition eval_Psatz  : list (NFormula Z) -> ZWitness ->  option (NFormula Z) :=
-  eval_Psatz 0 1 Zplus Zmult Zeq_bool Zle_bool.
+  eval_Psatz 0 1 Z.add Z.mul Zeq_bool Z.leb.
 
 
 Definition valid_cut_sign (op:Op1) :=
@@ -634,9 +625,9 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof)  {struct pf} : bool :
                    (fix label (pfs:list ZArithProof) :=
                    fun lb ub =>
                      match pfs with
-                       | nil => if Zgt_bool lb ub then true else false
-                       | pf::rsr => andb (ZChecker  ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub)
-                     end)   pf (Zopp z1)  z2
+                       | nil => if Z.gtb lb ub then true else false
+                       | pf::rsr => andb (ZChecker  ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub)
+                     end)   pf (Z.opp z1)  z2
                   else false
               |   _    ,   _   => true
            end
@@ -710,12 +701,12 @@ Proof.
   unfold makeCuttingPlane in H0.
   revert H0.
   case_eq (Zgcd_pol e) ; intros g c0.
-  generalize (Zgt_cases g 0) ; destruct (Zgt_bool g 0).
+  generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0).
   intros.
   inv H2.
-  change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in *.
+  change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *.
   apply Zgcd_pol_correct_lt with (env:=env) in H1.
-  generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Zminus e c0) g)) H0).
+  generalize (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0).
   auto with zarith.
   auto with zarith.
   (* g <= 0 *)
@@ -733,7 +724,7 @@ Proof.
   (* Equal *)
   destruct p as [[e' z] op].
   case_eq (Zgcd_pol e) ; intros g c.
-  case_eq (Zgt_bool g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Zgcd g c) g))) ; [discriminate|].
+  case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|].
   case_eq (makeCuttingPlane e).
   intros.
   inv H3.
@@ -741,7 +732,7 @@ Proof.
   rewrite H1 in H.
   revert H.
   change (eval_pol env e = 0) in H2.
-  case_eq (Zgt_bool g 0).
+  case_eq (Z.gtb g 0).
   intros.
   rewrite <- Zgt_is_gt_bool in H.  
   rewrite Zgcd_pol_correct_lt with (1:= H1)  in H2; auto with zarith.
@@ -749,7 +740,7 @@ Proof.
   change (eval_pol env (padd e' (Pc z)) = 0).
   inv H3.
   rewrite eval_pol_add.
-  set (x:=eval_pol env (Zdiv_pol (PsubC Zminus e c) g)) in *; clearbody x.
+  set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x.
   simpl.
   rewrite andb_false_iff in H0.
   destruct H0.
@@ -759,8 +750,7 @@ Proof.
   rewrite negb_false_iff in H0.
   apply Zeq_bool_eq in H0.
   subst. simpl.
-  rewrite Zplus_0_r in H2.
-  apply Zmult_integral in H2.
+  rewrite Z.add_0_r, Z.mul_eq_0 in H2.
   intuition auto with zarith.
   rewrite negb_false_iff in H0.
   apply Zeq_bool_eq in H0.
@@ -769,7 +759,7 @@ Proof.
   inv HH.
   apply Zdivide_opp_r in H4.
   rewrite Zdivide_ceiling ; auto.
-  apply Zeq_minus.
+  apply Z.sub_move_0_r.
   apply Z.div_unique_exact ; auto with zarith.
   intros.
   unfold nformula_of_cutting_plane.
@@ -789,7 +779,7 @@ Proof.
   simpl. auto with zarith.
   (* Strict *)
   destruct p as [[e' z] op].
-  case_eq (makeCuttingPlane (PsubC Zminus e 1)).
+  case_eq (makeCuttingPlane (PsubC Z.sub e 1)).
   intros.
   inv H1.
   apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
@@ -813,7 +803,7 @@ Proof.
   destruct f.
   destruct o.
   case_eq (Zgcd_pol p) ; intros g c.
-  case_eq (Zgt_bool g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Zgcd g c) g))).
+  case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))).
   intros.
   flatten_bool.
   rewrite negb_true_iff in H5.
@@ -823,16 +813,16 @@ Proof.
   apply Zeq_bool_neq in H.
   change (eval_pol env p = 0) in H2.
   rewrite Zgcd_pol_correct_lt with (1:= H0) in H2; auto with zarith.
-  set (x:=eval_pol env (Zdiv_pol (PsubC Zminus p c) g)) in *; clearbody x.
+  set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x.
   contradict H5.
   apply Zis_gcd_gcd; auto with zarith.
   constructor; auto with zarith.
   exists (-x).
-  rewrite <- Zopp_mult_distr_l, Zmult_comm; auto with zarith.
+  rewrite Z.mul_opp_l, Z.mul_comm; auto with zarith.
   (**)
   destruct (makeCuttingPlane p);  discriminate.
   discriminate.
-  destruct (makeCuttingPlane (PsubC Zminus p 1)) ; discriminate.
+  destruct (makeCuttingPlane (PsubC Z.sub p 1)) ; discriminate.
   destruct (makeCuttingPlane p) ; discriminate.
 Qed.
 
@@ -920,7 +910,7 @@ Proof.
    unfold nformula_of_cutting_plane in HCutR.
    unfold eval_nformula in HCutR.
    unfold RingMicromega.eval_nformula in HCutR.
-   change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in HCutR.
+   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR.
    unfold eval_op1 in HCutR.
    destruct op1 ; simpl in Hop1 ; try discriminate;
      rewrite eval_pol_add in HCutR; simpl in HCutR; auto with zarith.
@@ -933,7 +923,7 @@ Proof.
    unfold nformula_of_cutting_plane in HCutL.
    unfold eval_nformula in HCutL.
    unfold RingMicromega.eval_nformula in HCutL.
-   change (RingMicromega.eval_pol 0 Zplus Zmult (fun x : Z => x)) with eval_pol in HCutL.
+   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL.
    unfold eval_op1 in HCutL.
    rewrite eval_pol_add in HCutL. simpl in HCutL.
    destruct op2 ; simpl in Hop2 ; try discriminate ;  omega.
@@ -944,14 +934,14 @@ Proof.
   intros.
   assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
     (In pr pf /\
-      ZChecker  ((PsubC Zminus p1 x,Equal) :: l) pr = true)%Z).
+      ZChecker  ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z).
   clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1.
   revert Hfix.
   generalize (-z1). clear z1. intro z1.
   revert z1 z2.
   induction pf;simpl ;intros.
   generalize (Zgt_cases z1 z2).
-  destruct (Zgt_bool z1 z2).
+  destruct (Z.gtb z1 z2).
   intros.
   apply False_ind ; omega.
   discriminate.
@@ -972,7 +962,7 @@ Proof.
   zify. omega.
   (*/asser *)
   destruct (HH _ H1) as [pr [Hin Hcheker]].
-  assert (make_impl (eval_nformula env) ((PsubC Zminus p1 (eval_pol env p1),Equal) :: l) False).
+  assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False).
    apply (H pr);auto.
    apply in_bdepth ; auto.
   rewrite <- make_conj_impl in H2.
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 540d1b9c..25579a87 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -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/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 8b7ee55b..2020447f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -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        *)
@@ -300,6 +300,8 @@ struct
      ["Coq";"Reals" ; "Rpow_def"] ;
 ]
 
+  let z_modules = [["Coq";"ZArith";"BinInt"]]
+
   (**
     * Initialization : a large amount of Caml symbols are derived from
     * ZMicromega.v
@@ -309,6 +311,7 @@ struct
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
   let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
   let r_constant = gen_constant_in_modules "ZMicromega" r_modules
+  let z_constant = gen_constant_in_modules "ZMicromega" z_modules
   (* let constant = gen_constant_in_modules "Omicron" coq_modules *)
 
   let coq_and = lazy (init_constant "and")
@@ -371,17 +374,17 @@ struct
   let coq_cutProof = lazy (constant "CutProof")
   let coq_enumProof = lazy (constant "EnumProof")
 
-  let coq_Zgt = lazy (constant "Zgt")
-  let coq_Zge = lazy (constant "Zge")
-  let coq_Zle = lazy (constant "Zle")
-  let coq_Zlt = lazy (constant "Zlt")
+  let coq_Zgt = lazy (z_constant "Z.gt")
+  let coq_Zge = lazy (z_constant "Z.ge")
+  let coq_Zle = lazy (z_constant "Z.le")
+  let coq_Zlt = lazy (z_constant "Z.lt")
   let coq_Eq  = lazy (init_constant "eq")
 
-  let coq_Zplus = lazy (constant "Zplus")
-  let coq_Zminus = lazy (constant "Zminus")
-  let coq_Zopp = lazy (constant "Zopp")
-  let coq_Zmult = lazy (constant "Zmult")
-  let coq_Zpower = lazy (constant "Zpower")
+  let coq_Zplus = lazy (z_constant "Z.add")
+  let coq_Zminus = lazy (z_constant "Z.sub")
+  let coq_Zopp = lazy (z_constant "Z.opp")
+  let coq_Zmult = lazy (z_constant "Z.mul")
+  let coq_Zpower = lazy (z_constant "Z.pow")
 
   let coq_Qgt = lazy (constant "Qgt")
   let coq_Qge = lazy (constant "Qge")
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index 1604b0eb..dfda5984 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -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/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 3b6b6987..0d888f85 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.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        *)
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index c4dbf6af..ccbf0406 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -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/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index ed9fdcea..cb7a9280 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -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        *)
@@ -95,14 +95,24 @@ let read_key_elem inch =
     | End_of_file -> None
     |    _        -> raise InvalidTableFormat
 
+(** In win32, it seems that we should unlock the exact zone
+    that has been locked, and not the whole file *)
 
-let unlock fd = 
-  try 
-    let pos = lseek fd 0 SEEK_CUR in
-    ignore (lseek fd 0 SEEK_SET) ; 
-    lockf fd F_ULOCK 0 ; 
+let locked_start = ref 0
+
+let lock fd =
+  locked_start := lseek fd 0 SEEK_CUR;
+  lockf fd F_LOCK 0
+
+let rlock fd =
+  locked_start := lseek fd 0 SEEK_CUR;
+  lockf fd F_RLOCK 0
+
+let unlock fd =
+  let pos = lseek fd 0 SEEK_CUR in
+  ignore (lseek fd !locked_start SEEK_SET);
+  lockf fd F_ULOCK 0;
   ignore (lseek fd pos SEEK_SET)
-  with exc -> failwith (Printexc.to_string exc)
 
 let open_in f =
   let flags = [O_RDONLY ; O_CREAT] in
@@ -118,7 +128,7 @@ let open_in f =
 	  xload () in
     try
       (* Locking of the (whole) file while reading *)
-      lockf finch F_RLOCK 0 ; 
+      rlock finch;
       finally 
 	(fun () -> xload () ) 
 	(fun () -> 
@@ -136,7 +146,7 @@ let open_in f =
 	let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
 	let out =  (openfile f flags 0o666) in
 	let outch = out_channel_of_descr out in
-	  lockf out F_LOCK 0 ; 
+	  lock out;
 	  (try 
 	    Table.iter 
 	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
@@ -168,8 +178,8 @@ let add t k e =
       let fd = descr_of_out_channel outch in
       begin
 	Table.add tbl k e ;
-	lockf fd F_LOCK 0 ;
-	ignore (lseek fd 0 SEEK_END) ; 
+	lock fd;
+	ignore (lseek fd 0 SEEK_END);
 	Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
 	flush outch ;
 	unlock fd
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 14d312a5..36b05a72 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -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/micromega/sos.mli b/plugins/micromega/sos.mli
index 3d907e19..bc08d3c9 100644
--- a/plugins/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
@@ -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/micromega/sos_types.ml b/plugins/micromega/sos_types.ml
index 91aa5855..f9d2fb0b 100644
--- a/plugins/micromega/sos_types.ml
+++ b/plugins/micromega/sos_types.ml
@@ -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        *)