Imported Upstream version 8.5~beta1+dfsg

22 files changed, 1652 insertions, 1815 deletions

diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 92e61583..e7d0cd8e 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v
index 22448fd7..5dd1b86d 100644
--- a/plugins/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index f13f509a..4872c776 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -21,6 +21,7 @@ Require Export Ncring_tac.
 Class Cring {R:Type}`{Rr:Ring R} := 
  cring_mul_comm: forall x y:R, x * y == y * x.
 
+
 Ltac reify_goal lvar lexpr lterm:=
   (*idtac lvar; idtac lexpr; idtac lterm;*)
   match lexpr with
@@ -30,10 +31,10 @@ Ltac reify_goal lvar lexpr lterm:=
           |- (?op ?u1 ?u2) =>
            change (op 
              (@Ring_polynom.PEeval
-               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
                (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
              (@Ring_polynom.PEeval
-               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
                (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
         end
   end.
diff --git a/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v
index d2ab9e0f..4de2efe3 100644
--- a/plugins/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index 34a3018b..f867c6d0 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,55 +10,67 @@ Require Import Ring_tac BinList Ring_polynom InitialRing.
 Require Export Field_theory.
 
  (* syntaxification *)
- Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+ Ltac mkFieldexpr C Cst CstPow rO rI radd rmul rsub ropp rdiv rinv rpow t fv :=
  let rec mkP t :=
     let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with
+        | rO => 
+          fun _ => constr:(@FEO C)
+        | rI => 
+          fun _ => constr:(@FEI C)
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEadd e1 e2)
+          let e2 := mkP t2 in constr:(@FEadd C e1 e2)
         | (rmul ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEmul e1 e2)
+          let e2 := mkP t2 in constr:(@FEmul C e1 e2)
         | (rsub ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEsub e1 e2)
+          let e2 := mkP t2 in constr:(@FEsub C e1 e2)
         | (ropp ?t1) =>
-          fun _ => let e1 := mkP t1 in constr:(FEopp e1)
+          fun _ => let e1 := mkP t1 in constr:(@FEopp C e1)
         | (rdiv ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEdiv e1 e2)
+          let e2 := mkP t2 in constr:(@FEdiv C e1 e2)
         | (rinv ?t1) =>
-          fun _ => let e1 := mkP t1 in constr:(FEinv e1)
+          fun _ => let e1 := mkP t1 in constr:(@FEinv C e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant =>
             fun _ =>
             let p := Find_at t fv in
             constr:(@FEX C p)
-          | ?c => fun _ => let e1 := mkP t1 in constr:(FEpow e1 c)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(@FEpow C e1 c)
           end
         | _ =>
           fun _ =>
           let p := Find_at t fv in
           constr:(@FEX C p)
         end
-    | ?c => fun _ => constr:(FEc c)
+    | ?c => fun _ => constr:(@FEc C c)
     end in
     f ()
  in mkP t.
 
-Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac FFV Cst CstPow rO rI add mul sub opp div inv pow t fv :=
  let rec TFV t fv :=
   match Cst t with
   | InitialRing.NotConstant =>
       match t with
+      | rO => fv
+      | rI => fv
       | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
@@ -83,60 +95,60 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
 Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post :=
   let FLD :=
     match type of L1 with
-    | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
+    | context [req (@FEeval ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
                                       ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
         (fun proj =>
            proj Cst_tac Pow_tac pre post
-             req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
+             req rO rI radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
     | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
     end in
   F FLD.
 
 Ltac get_FldPre FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        pre).
 
 Ltac get_FldPost FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        post).
 
 Ltac get_L1 FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L1).
 
 Ltac get_SimplifyEqLemma FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L2).
 
 Ltac get_SimplifyLemma FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L3).
 
 Ltac get_L4 FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L4).
 
 Ltac get_CondLemma FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        cond_ok).
 
 Ltac get_FldEq FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        req).
 
@@ -146,33 +158,33 @@ Ltac get_FldCarrier FLD :=
 
 Ltac get_RingFV FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       FV Cst_tac Pow_tac radd rmul rsub ropp rpow).
+       FV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
 
 Ltac get_FFV FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+       FFV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
 
 Ltac get_RingMeta FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow).
+       mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
 
 Ltac get_Meta FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+       mkFieldexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
 
 Ltac get_Hyp_tac FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
+       let mkPol := mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow in
        fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
 
 Ltac get_FEeval FLD :=
@@ -180,8 +192,8 @@ Ltac get_FEeval FLD :=
   match type of L1 with
   | context
     [(@FEeval
-      ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
-       constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow)
+      ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
+       constr:(@FEeval R r0 r1 add mul sub opp div inv C phi Cpow powphi pow)
   | _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)"
   end.
 
@@ -201,8 +213,7 @@ Ltac fold_field_cond req :=
 Ltac simpl_PCond FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; 
-       clear lock_def lock);
+  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); 
   protect_fv "field_cond";
   fold_field_cond req;
   try exact I.
@@ -210,8 +221,7 @@ Ltac simpl_PCond FLD :=
 Ltac simpl_PCond_BEURK FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; 
-       clear lock_def lock);
+  (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req.
 
@@ -544,10 +554,9 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
          let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
          match s_spec with
          | mkhypo ?ss_spec =>
-           let field_ok3 := constr:(field_ok2 _ ss_spec) in
            match d_spec with
            | mkhypo ?dd_spec =>
-             let field_ok := constr:(field_ok3 _ dd_spec) in
+             let field_ok := constr:(field_ok2 _ dd_spec) in
              let mk_lemma lemma :=
               constr:(lemma _ _ _  _ _ _  _ _ _ _
                    set ext_r inv_m afth
@@ -563,7 +572,7 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
              (fun f =>
                f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
                   cond1_ok cond2_ok)
-           | _ => fail 4 "field: bad coefficiant division specification"
+           | _ => fail 4 "field: bad coefficient division specification"
            end
          | _ => fail 3 "field: bad sign specification"
          end
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 75d3ad86..0f5c49b0 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,123 +9,179 @@
 Require Ring.
 Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms.
 Require Import ZArith_base.
-(*Require Import Omega.*)
 Set Implicit Arguments.
+(* Set Universe Polymorphism. *)
 
 Section MakeFieldPol.
 
-(* Field elements *)
- Variable R:Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
- Variable (rdiv : R -> R ->  R) (rinv : R ->  R).
- Variable req : R -> R -> Prop.
-
- Notation "0" := rO. Notation "1" := rI.
- Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
- Notation "x - y " := (rsub x y). Notation "x / y" := (rdiv x y).
- Notation "- x" := (ropp x). Notation "/ x" := (rinv x).
- Notation "x == y" := (req x y) (at level 70, no associativity).
-
- (* Equality properties *)
- Variable Rsth : Equivalence req.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
- Variable SRinv_ext : forall p q, p == q ->  / p == / q.
-
- (* Field properties *)
-  Record almost_field_theory : Prop := mk_afield {
-    AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
-    AF_1_neq_0 : ~ 1 == 0;
-    AFdiv_def : forall p q, p / q == p * / q;
-    AFinv_l : forall p, ~ p == 0 ->  / p * p == 1
-  }.
+(* Field elements : R *)
+
+Variable R:Type.
+Bind Scope R_scope with R.
+Delimit Scope R_scope with ring.
+Local Open Scope R_scope.
+
+Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
+Variable (rdiv : R->R->R) (rinv : R->R).
+Variable req : R -> R -> Prop.
+
+Notation "0" := rO : R_scope.
+Notation "1" := rI : R_scope.
+Infix "+" := radd : R_scope.
+Infix "-" := rsub : R_scope.
+Infix "*" := rmul : R_scope.
+Infix "/" := rdiv : R_scope.
+Notation "- x" := (ropp x) : R_scope.
+Notation "/ x" := (rinv x) : R_scope.
+Infix "==" := req (at level 70, no associativity) : R_scope.
+
+(* Equality properties *)
+Variable Rsth : Equivalence req.
+Variable Reqe : ring_eq_ext radd rmul ropp req.
+Variable SRinv_ext : forall p q, p == q ->  / p == / q.
+
+(* Field properties *)
+Record almost_field_theory : Prop := mk_afield {
+ AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
+ AF_1_neq_0 : ~ 1 == 0;
+ AFdiv_def : forall p q, p / q == p * / q;
+ AFinv_l : forall p, ~ p == 0 ->  / p * p == 1
+}.
 
 Section AlmostField.
 
- Variable AFth : almost_field_theory.
- Let ARth := AFth.(AF_AR).
- Let rI_neq_rO := AFth.(AF_1_neq_0).
- Let rdiv_def := AFth.(AFdiv_def).
- Let rinv_l := AFth.(AFinv_l).
+Variable AFth : almost_field_theory.
+Let ARth := AFth.(AF_AR).
+Let rI_neq_rO := AFth.(AF_1_neq_0).
+Let rdiv_def := AFth.(AFdiv_def).
+Let rinv_l := AFth.(AFinv_l).
 
- (* Coefficients *)
- Variable C: Type.
- Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
- Variable ceqb : C->C->bool.
- Variable phi : C -> R.
+Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed.
+Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed.
+Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed.
+Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
+Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed.
 
- Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
-                               cO cI cadd cmul csub copp ceqb phi.
+Let eq_trans := Setoid.Seq_trans _ _ Rsth.
+Let eq_sym := Setoid.Seq_sym _ _ Rsth.
+Let eq_refl := Setoid.Seq_refl _ _ Rsth.
 
-Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
-  (phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y).
+Let radd_0_l := ARadd_0_l ARth.
+Let radd_comm := ARadd_comm ARth.
+Let radd_assoc := ARadd_assoc ARth.
+Let rmul_1_l := ARmul_1_l ARth.
+Let rmul_0_l := ARmul_0_l ARth.
+Let rmul_comm := ARmul_comm ARth.
+Let rmul_assoc := ARmul_assoc ARth.
+Let rdistr_l := ARdistr_l ARth.
+Let ropp_mul_l := ARopp_mul_l ARth.
+Let ropp_add := ARopp_add ARth.
+Let rsub_def := ARsub_def ARth.
+
+Let radd_0_r := ARadd_0_r Rsth ARth.
+Let rmul_0_r := ARmul_0_r Rsth ARth.
+Let rmul_1_r := ARmul_1_r Rsth ARth.
+Let ropp_0 := ARopp_zero Rsth Reqe ARth.
+Let rdistr_r := ARdistr_r Rsth Reqe ARth.
+
+(* Coefficients : C *)
+
+Variable C: Type.
+Bind Scope C_scope with C.
+Delimit Scope C_scope with coef.
+
+Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
+Variable ceqb : C->C->bool.
+Variable phi : C -> R.
+
+Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
+                              cO cI cadd cmul csub copp ceqb phi.
+
+Notation "0" := cO : C_scope.
+Notation "1" := cI : C_scope.
+Infix "+" := cadd : C_scope.
+Infix "-" := csub : C_scope.
+Infix "*" := cmul : C_scope.
+Notation "- x" := (copp x) : C_scope.
+Infix "=?" := ceqb : C_scope.
+Notation "[ x ]" := (phi x) (at level 0).
+
+Let phi_0 := CRmorph.(morph0).
+Let phi_1 := CRmorph.(morph1).
+
+Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef.
 Proof.
-intros.
-generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
-case (ceqb c1 c2); auto.
+generalize (CRmorph.(morph_eq) c c').
+destruct (c =? c')%coef; auto.
 Qed.
 
+(* Power coefficients : Cpow *)
 
- (* C notations *)
- Notation "x +! y" := (cadd x y) (at level 50).
- Notation "x *! y " := (cmul x y) (at level 40).
- Notation "x -! y " := (csub x y) (at level 50).
- Notation "-! x" := (copp x) (at level 35).
- Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity).
- Notation "[ x ]" := (phi x) (at level 0).
+Variable Cpow : Type.
+Variable Cp_phi : N -> Cpow.
+Variable rpow : R -> Cpow -> R.
+Variable pow_th : power_theory rI rmul req Cp_phi rpow.
+(* sign function *)
+Variable get_sign : C -> option C.
+Variable get_sign_spec : sign_theory copp ceqb get_sign.
 
+Variable cdiv:C -> C -> C*C.
+Variable cdiv_th : div_theory req cadd cmul phi cdiv.
 
- (* 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.
-  Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed.
+Let rpow_pow := pow_th.(rpow_pow_N).
 
-Let eq_trans := Setoid.Seq_trans _ _ Rsth.
-Let eq_sym := Setoid.Seq_sym _ _ Rsth.
-Let eq_refl := Setoid.Seq_refl _ _ Rsth.
+(* Polynomial expressions : (PExpr C) *)
+
+Bind Scope PE_scope with PExpr.
+Delimit Scope PE_scope with poly.
+
+Notation NPEeval := (PEeval rO rI radd rmul rsub ropp phi Cp_phi rpow).
+Notation "P @ l" := (NPEeval l P) (at level 10, no associativity).
+
+Arguments PEc _ _%coef.
+
+Notation "0" := (PEc 0) : PE_scope.
+Notation "1" := (PEc 1) : PE_scope.
+Infix "+" := PEadd : PE_scope.
+Infix "-" := PEsub : PE_scope.
+Infix "*" := PEmul : PE_scope.
+Notation "- e" := (PEopp e) : PE_scope.
+Infix "^" := PEpow : PE_scope.
+
+Definition NPEequiv e e' := forall l, e@l == e'@l.
+Infix "===" := NPEequiv (at level 70, no associativity) : PE_scope.
 
-Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) .
-Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe)
-             (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext.
-Hint Resolve (ARadd_0_l  ARth) (ARadd_comm  ARth) (ARadd_assoc ARth)
-             (ARmul_1_l  ARth) (ARmul_0_l  ARth)
-             (ARmul_comm  ARth) (ARmul_assoc ARth) (ARdistr_l  ARth)
-             (ARopp_mul_l ARth) (ARopp_add  ARth)
-             (ARsub_def  ARth) .
-
- (* 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.
- (* sign function *)
- Variable get_sign : C -> option C.
- Variable get_sign_spec : sign_theory copp ceqb get_sign.
-
- Variable cdiv:C -> C -> C*C.
- Variable cdiv_th : div_theory req cadd cmul phi cdiv.
-
-Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
-Notation Nnorm:= (norm_subst cO cI cadd cmul csub copp ceqb cdiv).
-
-Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
-Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign).
+Instance NPEequiv_eq : Equivalence NPEequiv.
+Proof.
+ split; red; unfold NPEequiv; intros; [reflexivity|symmetry|etransitivity];
+  eauto.
+Qed.
+
+Instance NPEeval_ext : Proper (eq ==> NPEequiv ==> req) NPEeval.
+Proof.
+ intros l l' <- e e' He. now rewrite (He l).
+Qed.
+
+Notation Nnorm :=
+  (norm_subst cO cI cadd cmul csub copp ceqb cdiv).
+Notation NPphi_dev :=
+  (Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
+Notation NPphi_pow :=
+  (Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign).
 
 (* add abstract semi-ring to help with some proofs *)
 Add Ring Rring : (ARth_SRth ARth).
 
-Local Hint Extern 2 (_ == _) => f_equiv.
-
 (* additional ring properties *)
 
-Lemma rsub_0_l : forall r, 0 - r == - r.
-intros; rewrite (ARsub_def ARth);ring.
+Lemma rsub_0_l r : 0 - r == - r.
+Proof.
+rewrite rsub_def; ring.
 Qed.
 
-Lemma rsub_0_r : forall r, r - 0 == r.
-intros; rewrite (ARsub_def ARth).
-rewrite (ARopp_zero Rsth Reqe ARth);  ring.
+Lemma rsub_0_r r : r - 0 == r.
+Proof.
+rewrite rsub_def, ropp_0; ring.
 Qed.
 
 (***************************************************************************
@@ -134,452 +190,525 @@ Qed.
 
   ***************************************************************************)
 
-Theorem rdiv_simpl: forall p q, ~ q == 0 ->  q * (p / q) == p.
+Theorem rdiv_simpl p q : ~ q == 0 ->  q * (p / q) == p.
 Proof.
-intros p q H.
+intros.
 rewrite rdiv_def.
-transitivity (/ q * q * p); [  ring | idtac ].
-rewrite rinv_l; auto.
+transitivity (/ q * q * p); [ ring | ].
+now rewrite rinv_l.
 Qed.
-Hint Resolve rdiv_simpl .
 
-Instance SRdiv_ext: Proper (req ==> req ==> req) rdiv.
+Instance rdiv_ext: Proper (req ==> req ==> req) rdiv.
 Proof.
-intros p1 p2 Ep q1 q2 Eq.
-transitivity (p1 * / q1); auto.
-transitivity (p2 * / q2); auto.
+intros p1 p2 Ep q1 q2 Eq. now rewrite !rdiv_def, Ep, Eq.
 Qed.
-Hint Resolve SRdiv_ext.
 
-Lemma rmul_reg_l : forall p q1 q2,
+Lemma rmul_reg_l p q1 q2 :
   ~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
 Proof.
-intros p q1 q2 H EQ.
-rewrite <- (@rdiv_simpl q1 p) by trivial.
-rewrite <- (@rdiv_simpl q2 p) by trivial.
-rewrite !rdiv_def, !(ARmul_assoc ARth).
-now rewrite EQ.
+intros H EQ.
+assert (H' : p * (q1 / p) == p * (q2 / p)).
+{ now rewrite !rdiv_def, !rmul_assoc, EQ. }
+now rewrite !rdiv_simpl in H'.
 Qed.
 
-Theorem field_is_integral_domain : forall r1 r2,
+Theorem field_is_integral_domain r1 r2 :
   ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
 Proof.
-intros r1 r2 H1 H2. contradict H2.
-transitivity (1 * r2); auto.
-transitivity (/ r1 * r1 * r2); auto.
-rewrite <- (ARmul_assoc ARth).
-rewrite H2.
-apply ARmul_0_r with (1 := Rsth) (2 := ARth).
+intros H1 H2. contradict H2.
+transitivity (/r1 * r1 * r2).
+- now rewrite rinv_l.
+- now rewrite <- rmul_assoc, H2.
 Qed.
 
-Theorem ropp_neq_0 : forall r,
+Theorem ropp_neq_0 r :
   ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0.
+Proof.
 intros.
 setoid_replace (- r) with (- (1) * r).
- apply field_is_integral_domain; trivial.
- rewrite <- (ARopp_mul_l ARth).
-   rewrite (ARmul_1_l ARth).
-   reflexivity.
+- apply field_is_integral_domain; trivial.
+- now rewrite <- ropp_mul_l, rmul_1_l.
 Qed.
 
-Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1.
-intros.
-rewrite (AFdiv_def AFth).
-rewrite (ARmul_comm ARth).
-apply (AFinv_l AFth).
-trivial.
+Theorem rdiv_r_r r : ~ r == 0 -> r / r == 1.
+Proof.
+intros. rewrite rdiv_def, rmul_comm. now apply rinv_l.
 Qed.
 
-Theorem rdiv1: forall r,  r == r / 1.
-intros r; transitivity (1 * (r / 1)); auto.
+Theorem rdiv1 r : r == r / 1.
+Proof.
+transitivity (1 * (r / 1)).
+- symmetry; apply rdiv_simpl. apply rI_neq_rO.
+- apply rmul_1_l.
 Qed.
 
-Theorem rdiv2:
- forall r1 r2 r3 r4,
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
+Theorem rdiv2 a b c d :
+ ~ b == 0 ->
+ ~ d == 0 ->
+ a / b + c / d == (a * d + c * b) / (b * d).
 Proof.
-intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-apply rmul_reg_l with (r2 * r4); trivial.
+intros H H0.
+assert (~ b * d == 0) by now apply field_is_integral_domain.
+apply rmul_reg_l with (b * d); trivial.
 rewrite rdiv_simpl; trivial.
-rewrite (ARdistr_r Rsth Reqe ARth).
-apply (Radd_ext Reqe).
-- transitivity (r2 * (r1 / r2) * r4); [  ring | auto ].
-- transitivity (r2 * (r4 * (r3 / r4))); auto.
-  transitivity (r2 * r3); auto.
+rewrite rdistr_r.
+apply radd_ext.
+- now rewrite <- rmul_assoc, (rmul_comm d), rmul_assoc, rdiv_simpl.
+- now rewrite (rmul_comm c), <- rmul_assoc, rdiv_simpl.
 Qed.
 
 
-Theorem rdiv2b:
- forall r1 r2 r3 r4 r5,
- ~ (r2*r5) == 0 ->
- ~ (r4*r5) == 0 ->
- r1 / (r2*r5) + r3 / (r4*r5) == (r1 * r4 + r3 * r2) / (r2 * (r4 * r5)).
+Theorem rdiv2b a b c d e :
+ ~ (b*e) == 0 ->
+ ~ (d*e) == 0 ->
+ a / (b*e) + c / (d*e) == (a * d + c * b) / (b * (d * e)).
 Proof.
-intros r1 r2 r3 r4 r5 H H0.
-assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring).
-assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring).
-assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring).
-assert (HH4: ~ r2 * (r4 * r5) == 0)
+intros H H0.
+assert (~ b == 0) by (contradict H; rewrite H; ring).
+assert (~ e == 0) by (contradict H; rewrite H; ring).
+assert (~ d == 0) by (contradict H0; rewrite H0; ring).
+assert (~ b * (d * e) == 0)
    by (repeat apply field_is_integral_domain; trivial).
-apply rmul_reg_l with (r2 * (r4 * r5)); trivial.
+apply rmul_reg_l with (b * (d * e)); trivial.
 rewrite rdiv_simpl; trivial.
-rewrite (ARdistr_r Rsth Reqe ARth).
-apply (Radd_ext Reqe).
- transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [  ring | auto ].
- transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [  ring | auto ].
-Qed.
-
-Theorem rdiv5: forall r1 r2,  - (r1 / r2) == - r1 / r2.
-Proof.
-intros r1 r2.
-transitivity (- (r1 * / r2)); auto.
-transitivity (- r1 * / r2); auto.
-Qed.
-Hint Resolve rdiv5 .
-
-Theorem rdiv3 r1 r2 r3 r4 :
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- r1 / r2 - r3 / r4 == (r1 * r4 -  r3 * r2) / (r2 * r4).
-Proof.
-intros H2 H4.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-transitivity (r1 / r2 + - (r3 / r4)); auto.
-transitivity (r1 / r2 + - r3 / r4); auto.
-transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)).
-apply rdiv2; auto.
-f_equiv.
-transitivity (r1 * r4 + - (r3 * r2)); auto.
-Qed.
-
-
-Theorem rdiv3b:
- forall r1 r2 r3 r4 r5,
- ~ (r2 * r5) == 0 ->
- ~ (r4 * r5) == 0 ->
- r1 / (r2*r5) - r3 / (r4*r5) == (r1 * r4 - r3 * r2) / (r2 * (r4 * r5)).
-Proof.
-intros r1 r2 r3 r4 r5 H H0.
-transitivity (r1 / (r2 * r5) + - (r3 / (r4 * r5))); auto.
-transitivity (r1 / (r2 * r5) + - r3 / (r4 * r5)); auto.
-transitivity ((r1 * r4 + - r3 * r2) / (r2 * (r4 * r5))).
-apply rdiv2b; auto; try ring.
-apply (SRdiv_ext); auto.
-transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
-Qed.
-
-Theorem rdiv6:
- forall r1 r2,
- ~ r1 == 0 -> ~ r2 == 0 ->  / (r1 / r2) == r2 / r1.
-intros r1 r2 H H0.
-assert (~ r1 / r2 == 0) as Hk.
- intros H1; case H.
-   transitivity (r2 * (r1 / r2)); auto.
-   rewrite H1;  ring.
- apply rmul_reg_l with (r1 / r2); auto.
-   transitivity (/ (r1 / r2) * (r1 / r2)); auto.
-   transitivity 1; auto.
-   repeat rewrite rdiv_def.
-   transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac |  ring ].
-   repeat rewrite rinv_l; auto.
-Qed.
-Hint Resolve rdiv6 .
-
- Theorem rdiv4:
- forall r1 r2 r3 r4,
- ~ r2 == 0 ->
- ~ r4 == 0 ->
- (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
-Proof.
-intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
-apply rmul_reg_l with (r2 * r4); trivial.
-rewrite rdiv_simpl; trivial.
-transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [  ring | idtac ].
-repeat rewrite rdiv_simpl; trivial.
+rewrite rdistr_r.
+apply radd_ext.
+- transitivity ((b * e) * (a / (b * e)) * d);
+  [ ring | now rewrite rdiv_simpl ].
+- transitivity ((d * e) * (c / (d * e)) * b);
+  [ ring | now rewrite rdiv_simpl ].
 Qed.
 
- Theorem rdiv4b:
- forall r1 r2 r3 r4 r5 r6,
- ~ r2 * r5 == 0 ->
- ~ r4 * r6 == 0 ->
- ((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4).
+Theorem rdiv5 a b : - (a / b) == - a / b.
 Proof.
-intros r1 r2 r3 r4 r5 r6 H H0.
-rewrite rdiv4; auto.
-transitivity ((r5 * r6) * (r1 * r3) / ((r5 * r6) * (r2 * r4))).
-apply SRdiv_ext; ring.
-assert (HH: ~ r5*r6 == 0).
-  apply field_is_integral_domain.
-    intros H1; case H; rewrite H1; ring.
-    intros H1; case H0; rewrite H1; ring.
-rewrite <- rdiv4 ; auto.
-  rewrite rdiv_r_r; auto.
+now rewrite !rdiv_def, ropp_mul_l.
+Qed.
 
-  apply field_is_integral_domain.
-    intros H1; case H; rewrite H1; ring.
-    intros H1; case H0; rewrite H1; ring.
+Theorem rdiv3b a b c d e :
+ ~ (b * e) == 0 ->
+ ~ (d * e) == 0 ->
+ a / (b*e) - c / (d*e) == (a * d - c * b) / (b * (d * e)).
+Proof.
+intros H H0.
+rewrite !rsub_def, rdiv5, ropp_mul_l.
+now apply rdiv2b.
 Qed.
 
+Theorem rdiv6 a b :
+ ~ a == 0 -> ~ b == 0 ->  / (a / b) == b / a.
+Proof.
+intros H H0.
+assert (Hk : ~ a / b == 0).
+{ contradict H.
+  transitivity (b * (a / b)).
+  - now rewrite rdiv_simpl.
+  - rewrite H. apply rmul_0_r. }
+apply rmul_reg_l with (a / b); trivial.
+rewrite (rmul_comm (a / b)), rinv_l; trivial.
+rewrite !rdiv_def.
+transitivity (/ a * a * (/ b * b)); [ | ring ].
+now rewrite !rinv_l, rmul_1_l.
+Qed.
+
+Theorem rdiv4 a b c d :
+ ~ b == 0 ->
+ ~ d == 0 ->
+ (a / b) * (c / d) == (a * c) / (b * d).
+Proof.
+intros H H0.
+assert (~ b * d == 0) by now apply field_is_integral_domain.
+apply rmul_reg_l with (b * d); trivial.
+rewrite rdiv_simpl; trivial.
+transitivity (b * (a / b) * (d * (c / d))); [ ring | ].
+rewrite !rdiv_simpl; trivial.
+Qed.
 
-Theorem rdiv7:
- forall r1 r2 r3 r4,
- ~ r2 == 0 ->
- ~ r3 == 0 ->
- ~ r4 == 0 ->
- (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3).
+Theorem rdiv4b a b c d e f :
+ ~ b * e == 0 ->
+ ~ d * f == 0 ->
+ ((a * f) / (b * e)) * ((c * e) / (d * f)) == (a * c) / (b * d).
+Proof.
+intros H H0.
+assert (~ b == 0) by (contradict H; rewrite H; ring).
+assert (~ e == 0) by (contradict H; rewrite H; ring).
+assert (~ d == 0) by (contradict H0; rewrite H0; ring).
+assert (~ f == 0) by (contradict H0; rewrite H0; ring).
+assert (~ b*d == 0) by now apply field_is_integral_domain.
+assert (~ e*f == 0) by now apply field_is_integral_domain.
+rewrite rdiv4; trivial.
+transitivity ((e * f) * (a * c) / ((e * f) * (b * d))).
+- apply rdiv_ext; ring.
+- rewrite <- rdiv4, rdiv_r_r; trivial.
+Qed.
+
+Theorem rdiv7 a b c d :
+ ~ b == 0 ->
+ ~ c == 0 ->
+ ~ d == 0 ->
+ (a / b) / (c / d) == (a * d) / (b * c).
 Proof.
 intros.
-rewrite (rdiv_def (r1 / r2)).
+rewrite (rdiv_def (a / b)).
 rewrite rdiv6; trivial.
 apply rdiv4; trivial.
 Qed.
 
-Theorem rdiv7b:
- forall r1 r2 r3 r4 r5 r6,
- ~ r2 * r6 == 0 ->
- ~ r3 * r5 == 0 ->
- ~ r4 * r6 == 0 ->
- ((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3).
+Theorem rdiv7b a b c d e f :
+ ~ b * f == 0 ->
+ ~ c * e == 0 ->
+ ~ d * f == 0 ->
+ ((a * e) / (b * f)) / ((c * e) / (d * f)) == (a * d) / (b * c).
+Proof.
+intros Hbf Hce Hdf.
+assert (~ c==0) by (contradict Hce; rewrite Hce; ring).
+assert (~ e==0) by (contradict Hce; rewrite Hce; ring).
+assert (~ b==0) by (contradict Hbf; rewrite Hbf; ring).
+assert (~ f==0) by (contradict Hbf; rewrite Hbf; ring).
+assert (~ b*c==0) by now apply field_is_integral_domain.
+assert (~ e*f==0) by now apply field_is_integral_domain.
+rewrite rdiv7; trivial.
+transitivity ((e * f) * (a * d) / ((e * f) * (b * c))).
+- apply rdiv_ext; ring.
+- now rewrite <- rdiv4, rdiv_r_r.
+Qed.
+
+Theorem rinv_nz a : ~ a == 0 -> ~ /a == 0.
+Proof.
+intros H H0. apply rI_neq_rO.
+rewrite <- (rdiv_r_r H), rdiv_def, H0. apply rmul_0_r.
+Qed.
+
+Theorem rdiv8 a b : ~ b == 0 -> a == 0 ->  a / b == 0.
+Proof.
+intros H H0.
+now rewrite rdiv_def, H0, rmul_0_l.
+Qed.
+
+Theorem cross_product_eq a b c d :
+  ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d.
 Proof.
 intros.
-rewrite rdiv7; auto.
-transitivity ((r5 * r6) * (r1 * r4) / ((r5 * r6) * (r2 * r3))).
-apply SRdiv_ext; ring.
-assert (HH: ~ r5*r6 == 0).
-  apply field_is_integral_domain.
-    intros H2; case H0; rewrite H2; ring.
-    intros H2; case H1; rewrite H2; ring.
-rewrite <- rdiv4 ; auto.
-rewrite rdiv_r_r; auto.
-  apply field_is_integral_domain.
-    intros H2; case H; rewrite H2; ring.
-    intros H2; case H0; rewrite H2; ring.
+transitivity (a / b * (d / d)).
+- now rewrite rdiv_r_r, rmul_1_r.
+- now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r.
 Qed.
 
+(* Results about [pow_pos] and [pow_N] *)
 
-Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 ->  r1 / r2 == 0.
-intros r1 r2 H H0.
-transitivity (r1 * / r2); auto.
-transitivity (0 * / r2); auto.
+Instance pow_ext : Proper (req ==> eq ==> req) (pow_pos rmul).
+Proof.
+intros x y H p p' <-.
+induction p as [p IH| p IH|];simpl; trivial; now rewrite !IH, ?H.
 Qed.
 
+Instance pow_N_ext : Proper (req ==> eq ==> req) (pow_N rI rmul).
+Proof.
+intros x y H n n' <-. destruct n; simpl; trivial. now apply pow_ext.
+Qed.
 
-Theorem cross_product_eq : forall r1 r2 r3 r4,
-  ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4.
-intros.
-transitivity (r1 / r2 * (r4 / r4)).
- rewrite rdiv_r_r; trivial.
-   symmetry .
-   apply (ARmul_1_r Rsth ARth).
- rewrite rdiv4; trivial.
-   rewrite H1.
-   rewrite (ARmul_comm ARth r2 r4).
-   rewrite <- rdiv4; trivial.
-   rewrite rdiv_r_r by trivial.
-  apply (ARmul_1_r Rsth ARth).
+Lemma pow_pos_0 p : pow_pos rmul 0 p == 0.
+Proof.
+induction p;simpl;trivial; now rewrite !IHp.
 Qed.
 
+Lemma pow_pos_1 p : pow_pos rmul 1 p == 1.
+Proof.
+induction p;simpl;trivial; ring [IHp].
+Qed.
+
+Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p].
+Proof.
+induction p;simpl;trivial; now rewrite !CRmorph.(morph_mul), !IHp.
+Qed.
+
+Lemma pow_pos_mul_l x y p :
+ pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
+Proof.
+induction p;simpl;trivial; ring [IHp].
+Qed.
+
+Lemma pow_pos_add_r x p1 p2 :
+ pow_pos rmul x (p1+p2) == pow_pos rmul x p1 * pow_pos rmul x p2.
+Proof.
+ exact (Ring_theory.pow_pos_add Rsth rmul_ext rmul_assoc x p1 p2).
+Qed.
+
+Lemma pow_pos_mul_r x p1 p2 :
+  pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2.
+Proof.
+induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r;
+ simpl; trivial; ring [IHp1].
+Qed.
+
+Lemma pow_pos_nz x p : ~x==0 -> ~pow_pos rmul x p == 0.
+Proof.
+ intros Hx. induction p;simpl;trivial;
+  repeat (apply field_is_integral_domain; trivial).
+Qed.
+
+Lemma pow_pos_div a b p : ~ b == 0 ->
+ pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p.
+Proof.
+ intros.
+ induction p; simpl; trivial.
+ - rewrite IHp.
+   assert (nz := pow_pos_nz p H).
+   rewrite !rdiv4; trivial.
+   apply field_is_integral_domain; trivial.
+ - rewrite IHp.
+   assert (nz := pow_pos_nz p H).
+   rewrite !rdiv4; trivial.
+Qed.
+
+(* === is a morphism *)
+
+Instance PEadd_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEadd C).
+Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed.
+Instance PEsub_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEsub C).
+Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed.
+Instance PEmul_ext : Proper (NPEequiv ==> NPEequiv ==> NPEequiv) (@PEmul C).
+Proof. intros ? ? E ? ? E' l. simpl. now rewrite E, E'. Qed.
+Instance PEopp_ext : Proper (NPEequiv ==> NPEequiv) (@PEopp C).
+Proof. intros ? ? E l. simpl. now rewrite E. Qed.
+Instance PEpow_ext : Proper (NPEequiv ==> eq ==> NPEequiv) (@PEpow C).
+Proof.
+ intros ? ? E ? ? <- l. simpl. rewrite !rpow_pow. apply pow_N_ext; trivial.
+Qed.
+
+Lemma PE_1_l (e : PExpr C) : (1 * e === e)%poly.
+Proof.
+ intros l. simpl. rewrite phi_1. apply rmul_1_l.
+Qed.
+
+Lemma PE_1_r (e : PExpr C) : (e * 1 === e)%poly.
+Proof.
+ intros l. simpl. rewrite phi_1. apply rmul_1_r.
+Qed.
+
+Lemma PEpow_0_r (e : PExpr C) : (e ^ 0 === 1)%poly.
+Proof.
+ intros l. simpl. now rewrite !rpow_pow.
+Qed.
+
+Lemma PEpow_1_r (e : PExpr C) : (e ^ 1 === e)%poly.
+Proof.
+ intros l. simpl. now rewrite !rpow_pow.
+Qed.
+
+Lemma PEpow_1_l n : (1 ^ n === 1)%poly.
+Proof.
+ intros l. simpl. rewrite rpow_pow. destruct n; simpl.
+ - now rewrite phi_1.
+ - now rewrite phi_1, pow_pos_1.
+Qed.
+
+Lemma PEpow_add_r (e : PExpr C) n n' :
+ (e ^ (n+n') === e ^ n * e ^ n')%poly.
+Proof.
+ intros l. simpl. rewrite !rpow_pow.
+ destruct n; simpl.
+ - rewrite rmul_1_l. trivial.
+ - destruct n'; simpl.
+   + rewrite rmul_1_r. trivial.
+   + apply pow_pos_add_r.
+Qed.
+
+Lemma PEpow_mul_l (e e' : PExpr C) n :
+ ((e * e') ^ n === e ^ n * e' ^ n)%poly.
+Proof.
+ intros l. simpl. rewrite !rpow_pow. destruct n; simpl; trivial.
+ - symmetry; apply rmul_1_l.
+ - apply pow_pos_mul_l.
+Qed.
+
+Lemma PEpow_mul_r (e : PExpr C) n n' :
+ (e ^ (n * n') === (e ^ n) ^ n')%poly.
+Proof.
+ intros l. simpl. rewrite !rpow_pow.
+ destruct n, n'; simpl; trivial.
+ - now rewrite pow_pos_1.
+ - apply pow_pos_mul_r.
+Qed.
+
+Lemma PEpow_nz l e n : ~ e @ l == 0 -> ~ (e^n) @ l == 0.
+Proof.
+ intros. simpl. rewrite rpow_pow. destruct n; simpl.
+ - apply rI_neq_rO.
+ - now apply pow_pos_nz.
+Qed.
+
+
 (***************************************************************************
 
                        Some equality test
 
   ***************************************************************************)
 
+Local Notation "a &&& b" := (if a then b else false)
+ (at level 40, left associativity).
+
 (* equality test *)
-Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
- match e1, e2 with
-   PEc c1, PEc c2 => ceqb c1 c2
-  | PEX p1, PEX p2 => Pos.eqb p1 p2
-  | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
-  | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
-  | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
-  | PEopp e3, PEopp e4 => PExpr_eq e3 e4
-  | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false
+Fixpoint PExpr_eq (e e' : PExpr C) {struct e} : bool :=
+ match e, e' with
+  | PEc c, PEc c' => ceqb c c'
+  | PEX _ p, PEX _ p' => Pos.eqb p p'
+  | e1 + e2, e1' + e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
+  | e1 - e2, e1' - e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
+  | e1 * e2, e1' * e2' => PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
+  | - e, - e' => PExpr_eq e e'
+  | e ^ n, e' ^ n' => N.eqb n n' &&& PExpr_eq e e'
   | _, _ => false
- end.
-
-Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph.
-intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH].
-Qed.
-
-Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph.
-intros x y H [|p];simpl;auto. apply pow_morph;trivial.
-Qed.
-
-Theorem PExpr_eq_semi_correct:
- forall l e1 e2, PExpr_eq e1 e2 = true ->  NPEeval l e1 == NPEeval l e2.
-intros l e1; elim e1.
-intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)).
-intros c2; apply (morph_eq CRmorph).
-intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)).
-intros p2; case Pos.eqb_spec; intros; now subst.
-intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
-intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
- (try (intros; discriminate)); auto.
-intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
-intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
- (try (intros; discriminate)); auto.
-intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
-intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
- (try (intros; discriminate)); auto.
-intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))).
-intros e4; generalize (rec e4); case (PExpr_eq e3 e4);
- (try (intros; discriminate)); auto.
-intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))).
-intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst.
-repeat rewrite  pow_th.(rpow_pow_N). rewrite (rec _ H);auto.
-Qed.
-
-(* add *)
-Definition NPEadd e1 e2 :=
-  match e1, e2 with
-    PEc c1, PEc c2 => PEc (cadd c1 c2)
-  | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2
-  |  _, PEc c => if ceqb c cO then e1 else PEadd e1 e2
-    (* Peut t'on factoriser ici ??? *)
-  | _, _ => PEadd e1 e2
-  end.
+ end%poly.
 
-Theorem NPEadd_correct:
- forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2).
+Lemma if_true (a b : bool) : a &&& b = true -> a = true /\ b = true.
 Proof.
-intros l e1 e2.
-destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c); simpl;try apply eq_refl;
- try (ring [(morph0 CRmorph)]).
- apply (morph_add CRmorph).
+ destruct a, b; split; trivial.
 Qed.
 
-Definition NPEpow x n :=
-  match n with
-  | N0 => PEc cI
-  | Npos p =>
-    if Pos.eqb p xH then x else
-    match x with
-    | PEc c =>
-      if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p)
-    | _ => PEpow x n
-    end
-  end.
-
-Theorem NPEpow_correct : forall l e n,
-  NPEeval l (NPEpow e n) == NPEeval l (PEpow e n).
+Theorem PExpr_eq_semi_ok e e' :
+ PExpr_eq e e' = true ->  (e === e')%poly.
+Proof.
+revert e'; induction e; destruct e'; simpl; try discriminate.
+- intros H l. now apply (morph_eq CRmorph).
+- case Pos.eqb_spec; intros; now subst.
+- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
+- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
+- intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
+- intros H. now rewrite IHe.
+- intros H. destruct (if_true _ _ H).
+  apply N.eqb_eq in H0. now rewrite IHe, H0.
+Qed.
+
+Lemma PExpr_eq_spec e e' : BoolSpec (e === e')%poly True (PExpr_eq e e').
 Proof.
- destruct n;simpl.
- rewrite pow_th.(rpow_pow_N);simpl;auto.
- fold (p =? 1)%positive.
- case Pos.eqb_spec; intros H; (rewrite H || clear H).
- now rewrite  pow_th.(rpow_pow_N).
- destruct e;simpl;auto.
- repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl.
- symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)].
- symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)].
- induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp].
+ assert (H := PExpr_eq_semi_ok e e').
+ destruct PExpr_eq; constructor; intros; trivial. now apply H.
 Qed.
 
-(* mul *)
-Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
-  match x, y with
-    PEc c1, PEc c2 => PEc (cmul c1 c2)
-  | PEc c, _ =>
-      if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y
-  |  _, PEc c =>
-      if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
-  | PEpow e1 n1, PEpow e2 n2 =>
-      if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
-  | _, _ => PEmul x y
-  end.
+(** Smart constructors for polynomial expression,
+    with reduction of constants *)
 
-Lemma pow_pos_mul : forall x y p, pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
-induction p;simpl;auto;try ring [IHp].
-Qed.
+Definition NPEadd e1 e2 :=
+  match e1, e2 with
+  | PEc c1, PEc c2 => PEc (c1 + c2)
+  | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2
+  |  _, PEc c => if (c =? 0)%coef then e1 else e1 + e2
+    (* Peut t'on factoriser ici ??? *)
+  | _, _ => (e1 + e2)
+  end%poly.
+Infix "++" := NPEadd (at level 60, right associativity).
 
-Theorem NPEmul_correct : forall l e1 e2,
-  NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2).
-induction e1;destruct e2; simpl;try reflexivity;
- repeat apply ceqb_rect;
- try (intro eq_c; rewrite eq_c); simpl; try reflexivity;
- try ring [(morph0 CRmorph) (morph1 CRmorph)].
- apply (morph_mul CRmorph).
-case N.eqb_spec; intros H; try rewrite <- H; clear H.
-rewrite NPEpow_correct. simpl.
-repeat rewrite pow_th.(rpow_pow_N).
-rewrite IHe1; destruct n;simpl;try ring.
-apply pow_pos_mul.
-simpl;auto.
+Theorem NPEadd_ok e1 e2 : (e1 ++ e2 === e1 + e2)%poly.
+Proof.
+intros l.
+destruct e1, e2; simpl; try reflexivity; try (case ceqb_spec);
+try intro H; try rewrite H; simpl;
+try apply eq_refl; try (ring [phi_0]).
+apply (morph_add CRmorph).
 Qed.
 
-(* sub *)
 Definition NPEsub e1 e2 :=
   match e1, e2 with
-    PEc c1, PEc c2 => PEc (csub c1 c2)
-  | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2
-  |  _, PEc c => if ceqb c cO then e1 else PEsub e1 e2
+  | PEc c1, PEc c2 => PEc (c1 - c2)
+  | PEc c, _ => if (c =? 0)%coef then - e2 else e1 - e2
+  |  _, PEc c => if (c =? 0)%coef then e1 else e1 - e2
      (* Peut-on factoriser ici *)
-  | _, _ => PEsub e1 e2
-  end.
+  | _, _ => e1 - e2
+  end%poly.
+Infix "--" := NPEsub (at level 50, left associativity).
 
-Theorem NPEsub_correct:
- forall l e1 e2,  NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2).
-intros l e1 e2.
-destruct e1; destruct e2; simpl; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c); simpl;
- try rewrite (morph0 CRmorph); try reflexivity;
+Theorem NPEsub_ok e1 e2: (e1 -- e2 === e1 - e2)%poly.
+Proof.
+intros l.
+destruct e1, e2; simpl; try reflexivity; try case ceqb_spec;
+ try intro H; try rewrite H; simpl;
+ try rewrite phi_0; try reflexivity;
  try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
 apply (morph_sub CRmorph).
 Qed.
 
-(* opp *)
 Definition NPEopp e1 :=
-  match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end.
+  match e1 with PEc c1 => PEc (- c1) | _ => - e1 end%poly.
+
+Theorem NPEopp_ok e : (NPEopp e === -e)%poly.
+Proof.
+intros l. destruct e; simpl; trivial. apply (morph_opp CRmorph).
+Qed.
+
+Definition NPEpow x n :=
+  match n with
+  | N0 => 1
+  | Npos p =>
+    if (p =? 1)%positive then x else
+    match x with
+    | PEc c =>
+      if (c =? 1)%coef then 1
+      else if (c =? 0)%coef then 0
+      else PEc (pow_pos cmul c p)
+    | _ => x ^ n
+    end
+  end%poly.
+Infix "^^" := NPEpow (at level 35, right associativity).
 
-Theorem NPEopp_correct:
- forall l e1,  NPEeval l (NPEopp e1) == NPEeval l (PEopp e1).
-intros l e1; case e1; simpl; auto.
-intros; apply (morph_opp CRmorph).
+Theorem NPEpow_ok e n : (e ^^ n === e ^ n)%poly.
+Proof.
+ intros l. unfold NPEpow; destruct n.
+ - simpl; now rewrite rpow_pow.
+ - case Pos.eqb_spec; [intro; subst | intros _].
+   + simpl. now rewrite rpow_pow.
+   + destruct e;simpl;trivial.
+     repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl.
+     * now rewrite phi_1, pow_pos_1.
+     * now rewrite phi_0, pow_pos_0.
+     * now rewrite pow_pos_cst.
+Qed.
+
+Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
+  match x, y with
+  | PEc c1, PEc c2 => PEc (c1 * c2)
+  | PEc c, _ => if (c =? 1)%coef then y else if (c =? 0)%coef then 0 else x * y
+  | _, PEc c => if (c =? 1)%coef then x else if (c =? 0)%coef then 0 else x * y
+  | e1 ^ n1, e2 ^ n2 => if (n1 =? n2)%N then (NPEmul e1 e2)^^n1 else x * y
+  | _, _ => x * y
+  end%poly.
+Infix "**" := NPEmul (at level 40, left associativity).
+
+Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly.
+Proof.
+intros l.
+revert e2; induction e1;destruct e2; simpl;try reflexivity;
+ repeat (case ceqb_spec; intro H; try rewrite H; clear H);
+ simpl; try reflexivity; try ring [phi_0 phi_1].
+ apply (morph_mul CRmorph).
+case N.eqb_spec; [intros <- | reflexivity].
+rewrite NPEpow_ok. simpl.
+rewrite !rpow_pow. rewrite IHe1.
+destruct n; simpl; [ ring | apply pow_pos_mul_l ].
 Qed.
 
 (* simplification *)
-Fixpoint PExpr_simp (e : PExpr C) : PExpr C :=
+Fixpoint PEsimp (e : PExpr C) : PExpr C :=
  match e with
-   PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2)
-  | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2)
-  | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2)
-  | PEopp e1 => NPEopp (PExpr_simp e1)
-  | PEpow e1 n1 => NPEpow (PExpr_simp e1) n1
+  | e1 + e2 => (PEsimp e1) ++ (PEsimp e2)
+  | e1 * e2 => (PEsimp e1) ** (PEsimp e2)
+  | e1 - e2 => (PEsimp e1) -- (PEsimp e2)
+  | - e1 => NPEopp (PEsimp e1)
+  | e1 ^ n1 => (PEsimp e1) ^^ n1
   | _ => e
- end.
+ end%poly.
 
-Theorem PExpr_simp_correct:
- forall l e,  NPEeval l (PExpr_simp e) == NPEeval l e.
-intros l e; elim e; simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEadd_correct.
-simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEsub_correct.
-simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEmul_correct.
-simpl; auto.
-intros e1 He1.
-transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto.
-apply NPEopp_correct.
-simpl; auto.
-intros e1 He1 n;simpl.
-rewrite NPEpow_correct;simpl.
-repeat rewrite pow_th.(rpow_pow_N).
-rewrite He1;auto.
+Theorem PEsimp_ok e : (PEsimp e === e)%poly.
+Proof.
+induction e; simpl.
+- reflexivity.
+- reflexivity.
+- intro l; trivial.
+- intro l; trivial.
+- rewrite NPEadd_ok. now f_equiv.
+- rewrite NPEsub_ok. now f_equiv.
+- rewrite NPEmul_ok. now f_equiv.
+- rewrite NPEopp_ok. now f_equiv.
+- rewrite NPEpow_ok. now f_equiv.
 Qed.
 
 
@@ -592,7 +721,9 @@ Qed.
 (* The input: syntax of a field expression *)
 
 Inductive FExpr : Type :=
-   FEc: C ->  FExpr
+ | FEO : FExpr
+ | FEI : FExpr
+ | FEc: C ->  FExpr
  | FEX: positive ->  FExpr
  | FEadd: FExpr -> FExpr ->  FExpr
  | FEsub: FExpr -> FExpr ->  FExpr
@@ -604,6 +735,8 @@ Inductive FExpr : Type :=
 
 Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
   match pe with
+  | FEO       => rO
+  | FEI       => rI
   | FEc c     => phi c
   | FEX x     => BinList.nth 0 x l
   | FEadd x y => FEeval l x + FEeval l y
@@ -633,44 +766,46 @@ Record linear : Type := mk_linear {
 Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop :=
   match le with
   | nil => True
-  | e1 :: nil => ~ req (NPEeval l e1) rO
-  | e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1
+  | e1 :: nil => ~ req (e1 @ l) rO
+  | e1 :: l1 => ~ req (e1 @ l) rO /\ PCond l l1
   end.
 
-Theorem PCond_cons_inv_l :
-   forall l a l1, PCond l (a::l1) ->  ~ NPEeval l a == 0.
-intros l a l1 H.
-destruct l1; simpl in H |- *; trivial.
-destruct H; trivial.
+Theorem PCond_cons l a l1 :
+ PCond l (a :: l1) <-> ~ a @ l == 0 /\ PCond l l1.
+Proof.
+destruct l1.
+- simpl. split; [split|destruct 1]; trivial.
+- reflexivity.
 Qed.
 
-Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) ->  PCond l l1.
-intros l a l1 H.
-destruct l1; simpl in H |- *; trivial.
-destruct H; trivial.
+Theorem PCond_cons_inv_l l a l1 : PCond l (a::l1) ->  ~ a @ l == 0.
+Proof.
+rewrite PCond_cons. now destruct 1.
 Qed.
 
-Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l1.
-intros l l1 l2; elim l1; simpl app.
- simpl; auto.
- destruct l0; simpl in *.
-  destruct l2; firstorder.
-  firstorder.
+Theorem PCond_cons_inv_r l a l1 : PCond l (a :: l1) ->  PCond l l1.
+Proof.
+rewrite PCond_cons. now destruct 1.
 Qed.
 
-Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l2.
-intros l l1 l2; elim l1; simpl app; auto.
-intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ).
+Theorem PCond_app l l1 l2 :
+ PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2.
+Proof.
+induction l1.
+- simpl. split; [split|destruct 1]; trivial.
+- simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc.
 Qed.
 
+
 (* An unsatisfiable condition: issued when a division by zero is detected *)
-Definition absurd_PCond := cons (PEc cO) nil.
+Definition absurd_PCond := cons 0%poly nil.
 
 Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
+Proof.
 unfold absurd_PCond; simpl.
 red; intros.
 apply H.
-apply (morph0 CRmorph).
+apply phi_0.
 Qed.
 
 (***************************************************************************
@@ -679,167 +814,124 @@ Qed.
 
   ***************************************************************************)
 
-Fixpoint isIn (e1:PExpr C)  (p1:positive)
-                      (e2:PExpr C)  (p2:positive) {struct e2}: option (N * PExpr C) :=
+Definition default_isIn e1 p1 e2 p2 :=
+  if PExpr_eq e1 e2 then
+    match Z.pos_sub p1 p2 with
+     | Zpos p => Some (Npos p, 1%poly)
+     | Z0 => Some (N0, 1%poly)
+     | Zneg p => Some (N0, e2 ^^ Npos p)
+    end
+  else None.
+
+Fixpoint isIn e1 p1 e2 p2 {struct e2}: option (N * PExpr C) :=
   match e2 with
-  | PEmul e3 e4 =>
+  | e3 * e4 =>
        match isIn e1 p1 e3 p2 with
-       | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2)))
+       | Some (N0, e5) => Some (N0, e5 ** (e4 ^^ Npos p2))
        | Some (Npos p, e5) =>
           match isIn e1 p e4 p2 with
-          | Some (n, e6) => Some (n, NPEmul e5 e6)
-          | None => Some (Npos p, NPEmul e5 (NPEpow e4 (Npos p2)))
+          | Some (n, e6) => Some (n, e5 ** e6)
+          | None => Some (Npos p, e5 ** (e4 ^^ Npos p2))
           end
        | None =>
          match isIn e1 p1 e4 p2 with
-         | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5)
+         | Some (n, e5) => Some (n, (e3 ^^ Npos p2) ** e5)
          | None => None
          end
        end
-  | PEpow e3 N0 => None
-  | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pos.mul p3 p2)
-  | _ =>
-     if  PExpr_eq e1 e2 then
-         match Z.pos_sub p1 p2 with
-          | Zpos p => Some (Npos p, PEc cI)
-          | Z0 => Some (N0, PEc cI)
-          | Zneg p => Some (N0, NPEpow e2 (Npos p))
-          end
-     else None
-   end.
+  | e3 ^ N0 => None
+  | e3 ^ Npos p3 => isIn e1 p1 e3 (Pos.mul p3 p2)
+  | _ => default_isIn e1 p1 e2 p2
+   end%poly.
 
  Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end.
  Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end.
 
- Notation pow_pos_add :=
-   (Ring_theory.pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
-
  Lemma Z_pos_sub_gt p q : (p > q)%positive ->
   Z.pos_sub p q = Zpos (p - q).
  Proof. intros; now apply Z.pos_sub_gt, Pos.gt_lt. Qed.
 
  Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
 
- Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
-  match
-      (if  PExpr_eq e1 e2 then
-         match Z.sub (Zpos p1) (Zpos p2) with
-          | Zpos p => Some (Npos p, PEc cI)
-          | Z0 => Some (N0, PEc cI)
-          | Zneg p => Some (N0, NPEpow e2 (Npos p))
-          end
-     else None)
-   with
+ Lemma default_isIn_ok e1 e2 p1 p2 :
+  match default_isIn e1 p1 e2 p2 with
    | Some(n, e3) =>
-       NPEeval l (PEpow e2 (Npos p2)) ==
-       NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\
-       (Zpos p1 > NtoZ n)%Z
-   |  _ => True
+       let n' := ZtoN (Zpos p1 - NtoZ n) in
+       (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly
+       /\ (Zpos p1 > NtoZ n)%Z
+   | _ => True
   end.
 Proof.
-  intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
-   case (PExpr_eq e1 e2); simpl; auto; intros H.
+  unfold default_isIn.
+  case PExpr_eq_spec; trivial. intros EQ.
   rewrite Z.pos_sub_spec.
-  case Pos.compare_spec;intros;simpl.
-  - repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:reflexivity.
-    subst. rewrite H by trivial. ring [ (morph1 CRmorph)].
-  - fold (p2 - p1 =? 1)%positive.
-    fold (NPEpow e2 (Npos (p2 - p1))).
-    rewrite NPEpow_correct;simpl.
-    repeat rewrite pow_th.(rpow_pow_N);simpl.
-    rewrite H;trivial. split. 2:reflexivity.
-    rewrite <- pow_pos_add. now rewrite Pos.add_comm, Pos.sub_add.
-  - repeat rewrite pow_th.(rpow_pow_N);simpl.
-    rewrite H;trivial.
-    rewrite Z.pos_sub_gt by now apply Pos.sub_decr.
-    replace (p1 - (p1 - p2))%positive with p2;
-    [| rewrite Pos.sub_sub_distr, Pos.add_comm;
-       auto using Pos.add_sub, Pos.sub_decr ].
-    split.
-    simpl. ring [ (morph1 CRmorph)].
-    now apply Z.lt_gt, Pos.sub_decr.
-Qed.
-
-Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
-induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_add;simpl.
-ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto.
-Qed.
-
-
-Theorem isIn_correct: forall l e1 p1 e2 p2,
+  case Pos.compare_spec;intros H; split; try reflexivity.
+  - simpl. now rewrite PE_1_r, H, EQ.
+  - rewrite NPEpow_ok, EQ, <- PEpow_add_r. f_equiv.
+    simpl. f_equiv. now rewrite Pos.add_comm, Pos.sub_add.
+  - simpl. rewrite PE_1_r, EQ. f_equiv.
+    rewrite Z.pos_sub_gt by now apply Pos.sub_decr. simpl. f_equiv.
+    rewrite Pos.sub_sub_distr, Pos.add_comm; trivial.
+    rewrite Pos.add_sub; trivial.
+    apply Pos.sub_decr; trivial.
+  - simpl. now apply Z.lt_gt, Pos.sub_decr.
+Qed.
+
+Ltac npe_simpl := rewrite ?NPEmul_ok, ?NPEpow_ok, ?PEpow_mul_l.
+Ltac npe_ring := intro l; simpl; ring.
+
+Theorem isIn_ok e1 p1 e2 p2 :
   match isIn e1 p1 e2 p2 with
    | Some(n, e3) =>
-       NPEeval l (PEpow e2 (Npos p2)) ==
-       NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\
-        (Zpos p1 > NtoZ n)%Z
+       let n' := ZtoN (Zpos p1 - NtoZ n) in
+       (e2 ^ N.pos p2 === e1 ^ n' * e3)%poly
+       /\ (Zpos p1 > NtoZ n)%Z
    |  _ => True
   end.
 Proof.
 Opaque NPEpow.
-intros l e1 p1 e2; generalize p1;clear p1;elim e2; intros;
-  try (refine (isIn_correct_aux l e1 _ p1 p2);fail);simpl isIn.
-generalize (H p1 p2);clear H;destruct (isIn e1 p1 p p2). destruct p3.
-destruct n.
-  simpl. rewrite NPEmul_correct. simpl; rewrite NPEpow_correct;simpl.
-  repeat rewrite pow_th.(rpow_pow_N);simpl.
-  rewrite pow_pos_mul;intros (H,H1);split;[ring[H]|trivial].
-  generalize (H0 p4 p2);clear H0;destruct (isIn e1 p4 p0 p2). destruct p5.
-  destruct n;simpl.
-    rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
-    intros (H1,H2) (H3,H4).
-    simpl_pos_sub. simpl in H3.
-    rewrite pow_pos_mul. rewrite H1;rewrite H3.
-    assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
-        (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
-        pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) *
-        NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H.
-   rewrite <- pow_pos_add.
-   rewrite Pos.add_comm, Pos.sub_add by (now apply Z.gt_lt in H4).
-   split. symmetry;apply ARth.(ARmul_assoc). reflexivity.
-   repeat rewrite pow_th.(rpow_pow_N);simpl.
-   intros (H1,H2) (H3,H4).
-   simpl_pos_sub. simpl in H1, H3.
-   assert (Zpos p1 > Zpos p6)%Z.
-     apply Zgt_trans with (Zpos p4). exact H4. exact H2.
-  simpl_pos_sub.
-  split. 2:exact H.
-  rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
-  assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
-                (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) ==
-             pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) *
-                NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0.
-  rewrite <- pow_pos_add.
-  replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive.
- rewrite NPEmul_correct. simpl;ring.
-  assert
-     (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
- change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
- rewrite <- Z.add_assoc. rewrite (Z.add_assoc  (- Zpos p4)).
- simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
- unfold Z.sub, Z.opp in H0. simpl in H0.
-  simpl_pos_sub. inversion H0; trivial.
- simpl. repeat rewrite pow_th.(rpow_pow_N).
- intros H1 (H2,H3). simpl_pos_sub.
- rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
- simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
- rewrite pow_pos_mul. split. ring [H2]. exact H3.
- generalize (H0 p1 p2);clear H0;destruct (isIn e1 p1 p0 p2). destruct p3.
- destruct n;simpl. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
- repeat rewrite pow_th.(rpow_pow_N);simpl.
- intros (H1,H2);split;trivial. rewrite pow_pos_mul;ring [H1].
- rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
- repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
- intros (H1, H2);rewrite H1;split.
-   simpl_pos_sub. simpl in H1;ring [H1]. trivial.
- trivial.
- destruct n. trivial.
- generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
- destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl.
- intros (H1,H2);split. rewrite pow_pos_pow_pos. trivial. trivial.
- repeat rewrite pow_th.(rpow_pow_N). simpl.
- intros (H1,H2);split;trivial.
- rewrite pow_pos_pow_pos;trivial.
- trivial.
+revert p1 p2.
+induction e2; intros p1 p2;
+ try refine (default_isIn_ok e1 _ p1 p2); simpl isIn.
+- specialize (IHe2_1 p1 p2).
+  destruct isIn as [([|p],e)|].
+  + split; [|reflexivity].
+    clear IHe2_2.
+    destruct IHe2_1 as (IH,_).
+    npe_simpl. rewrite IH. npe_ring.
+  + specialize (IHe2_2 p p2).
+    destruct isIn as [([|p'],e')|].
+    * destruct IHe2_1 as (IH1,GT1).
+      destruct IHe2_2 as (IH2,GT2).
+      split; [|simpl; apply Zgt_trans with (Z.pos p); trivial].
+      npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl.
+      replace (N.pos p1) with (N.pos p + N.pos (p1 - p))%N.
+      rewrite PEpow_add_r; npe_ring.
+      { simpl. f_equal. rewrite Pos.add_comm, Pos.sub_add. trivial.
+        now apply Pos.gt_lt. }
+    * destruct IHe2_1 as (IH1,GT1).
+      destruct IHe2_2 as (IH2,GT2).
+      assert (Z.pos p1 > Z.pos p')%Z by (now apply Zgt_trans with (Zpos p)).
+      split; [|simpl; trivial].
+      npe_simpl. rewrite IH1, IH2. simpl. simpl_pos_sub. simpl.
+      replace (N.pos (p1 - p')) with (N.pos (p1 - p) + N.pos (p - p'))%N.
+      rewrite PEpow_add_r; npe_ring.
+      { simpl. f_equal. rewrite Pos.add_sub_assoc, Pos.sub_add; trivial.
+        now apply Pos.gt_lt.
+        now apply Pos.gt_lt. }
+    * destruct IHe2_1 as (IH,GT). split; trivial.
+      npe_simpl. rewrite IH. npe_ring.
+  + specialize (IHe2_2 p1 p2).
+    destruct isIn as [(n,e)|]; trivial.
+    destruct IHe2_2 as (IH,GT). split; trivial.
+    set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
+    npe_simpl. rewrite IH. npe_ring.
+- destruct n; trivial.
+  specialize (IHe2 p1 (p * p2)%positive).
+  destruct isIn as [(n,e)|]; trivial.
+  destruct IHe2 as (IH,GT). split; trivial.
+  set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
+  now rewrite <- PEpow_mul_r.
 Qed.
 
 Record rsplit : Type := mk_rsplit {
@@ -852,121 +944,122 @@ Notation left := rsplit_left.
 Notation right := rsplit_right.
 Notation common := rsplit_common.
 
-Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit :=
+Fixpoint split_aux e1 p e2 {struct e1}: rsplit :=
   match e1 with
-  | PEmul e3 e4 =>
+  | e3 * e4 =>
       let r1 := split_aux e3 p e2 in
       let r2 := split_aux e4 p (right r1) in
-          mk_rsplit (NPEmul (left r1) (left r2))
-                    (NPEmul (common r1) (common r2))
-                    (right r2)
-  | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2
-  | PEpow e3 (Npos p3) => split_aux e3 (Pos.mul p3 p) e2
+      mk_rsplit (left r1 ** left r2)
+                (common r1 ** common r2)
+                (right r2)
+  | e3 ^ N0 => mk_rsplit 1 1 e2
+  | e3 ^ Npos p3 => split_aux e3 (Pos.mul p3 p) e2
   | _ =>
-       match isIn e1 p e2 xH with
-       | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
-       | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
-       | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2
+       match isIn e1 p e2 1 with
+       | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3
+       | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3
+       | None => mk_rsplit (e1 ^^ Npos p) 1 e2
        end
-  end.
+  end%poly.
 
-Lemma split_aux_correct_1 : forall l e1 p e2,
-  let res :=  match isIn e1 p e2 xH with
-       | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
-       | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
-       | None => mk_rsplit (NPEpow e1  (Npos p)) (PEc cI) e2
-       end in
-       NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res))
-   /\
-       NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)).
-Proof.
- intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH).
- destruct (isIn e1 p e2 1). destruct p0.
+Lemma split_aux_ok1 e1 p e2 :
+  (let res := match isIn e1 p e2 1 with
+       | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3
+       | Some (Npos q, e3) => mk_rsplit (e1 ^^ Npos q) (e1 ^^ Npos (p - q)) e3
+       | None => mk_rsplit (e1 ^^ Npos p) 1 e2
+       end
+  in
+  e1 ^ Npos p === left res * common res
+  /\ e2 === right res * common res)%poly.
+Proof.
  Opaque NPEpow NPEmul.
-  destruct n;simpl;
-    (repeat rewrite NPEmul_correct;simpl;
-     repeat rewrite NPEpow_correct;simpl;
-     repeat rewrite pow_th.(rpow_pow_N);simpl).
-  intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
-  intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
-  apply Z.gt_lt in Hgt.
-  now rewrite <- pow_pos_add, Pos.add_comm, Pos.sub_add.
-  simpl;intros. repeat rewrite NPEmul_correct;simpl.
-  rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
-Qed.
-
-Theorem split_aux_correct: forall l e1 p e2,
-  NPEeval l (PEpow e1 (Npos p)) ==
-       NPEeval l (NPEmul (left (split_aux e1 p e2)) (common (split_aux e1 p e2)))
-/\
-  NPEeval l  e2 == NPEeval l (NPEmul (right (split_aux e1 p e2))
-                                   (common (split_aux e1 p e2))).
-Proof.
-intros l; induction e1;intros k e2; try refine (split_aux_correct_1 l _ k e2);simpl.
-generalize (IHe1_1 k e2); clear IHe1_1.
-generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2.
-simpl. repeat (rewrite NPEmul_correct;simpl).
-repeat rewrite pow_th.(rpow_pow_N);simpl.
-intros (H1,H2) (H3,H4);split.
-rewrite pow_pos_mul. rewrite H1;rewrite H3. ring.
-rewrite H4;rewrite H2;ring.
-destruct n;simpl.
-split. repeat rewrite pow_th.(rpow_pow_N);simpl.
-rewrite NPEmul_correct. simpl.
- induction k;simpl;try ring [CRmorph.(morph1)]; ring [IHk CRmorph.(morph1)].
- rewrite NPEmul_correct;simpl. ring [CRmorph.(morph1)].
-generalize (IHe1 (p*k)%positive e2);clear IHe1;simpl.
-repeat rewrite NPEmul_correct;simpl.
-repeat rewrite pow_th.(rpow_pow_N);simpl.
-rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2].
+ intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
+ destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl.
+ - intros (H1,H2); split; npe_simpl.
+   + now rewrite PE_1_l.
+   + rewrite PEpow_1_r in H1. rewrite H1. npe_ring.
+ - intros (H1,H2); split; npe_simpl.
+   + rewrite <- PEpow_add_r. f_equiv. simpl. f_equal.
+     rewrite Pos.add_comm, Pos.sub_add; trivial.
+     now apply Z.gt_lt in H2.
+   + rewrite PEpow_1_r in H1. rewrite H1. simpl_pos_sub. simpl. npe_ring.
+ - intros _; split; npe_simpl; now rewrite PE_1_r.
+Qed.
+
+Theorem split_aux_ok: forall e1 p e2,
+  (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2)
+  /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly.
+Proof.
+induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl.
+destruct (IHe1_1 k e2) as (H1,H2).
+destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4).
+clear IHe1_1 IHe1_2.
+- npe_simpl; split.
+  * rewrite H1, H3. npe_ring.
+  * rewrite H2 at 1. rewrite H4 at 1. npe_ring.
+- destruct n; simpl.
+  + rewrite PEpow_0_r, PEpow_1_l, !PE_1_r. now split.
+  + rewrite <- PEpow_mul_r. simpl. apply IHe1.
 Qed.
 
 Definition split e1 e2 := split_aux e1 xH e2.
 
-Theorem split_correct_l: forall l e1 e2,
-  NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2))
-                                   (common (split e1 e2))).
+Theorem split_ok_l e1 e2 :
+  (e1 === left (split e1 e2) * common (split e1 e2))%poly.
+Proof.
+destruct (split_aux_ok e1 xH e2) as (H,_). now rewrite <- H, PEpow_1_r.
+Qed.
+
+Theorem split_ok_r e1 e2 :
+  (e2 === right (split e1 e2) * common (split e1 e2))%poly.
 Proof.
-intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl.
-rewrite pow_th.(rpow_pow_N);simpl;auto.
+destruct (split_aux_ok e1 xH e2) as (_,H). trivial.
 Qed.
 
-Theorem split_correct_r: forall l e1 e2,
-  NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
-                                   (common (split e1 e2))).
+Lemma split_nz_l l e1 e2 :
+ ~ e1 @ l == 0 -> ~ left (split e1 e2) @ l == 0.
 Proof.
-intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto.
+ intros H. contradict H. rewrite (split_ok_l e1 e2); simpl.
+ now rewrite H, rmul_0_l.
+Qed.
+
+Lemma split_nz_r l e1 e2 :
+ ~ e2 @ l == 0 -> ~ right (split e1 e2) @ l == 0.
+Proof.
+ intros H. contradict H. rewrite (split_ok_r e1 e2); simpl.
+ now rewrite H, rmul_0_l.
 Qed.
 
 Fixpoint Fnorm (e : FExpr) : linear :=
   match e with
-  | FEc c => mk_linear (PEc c) (PEc cI) nil
-  | FEX x => mk_linear (PEX C x) (PEc cI) nil
+  | FEO => mk_linear 0 1 nil
+  | FEI => mk_linear 1 1 nil
+  | FEc c => mk_linear (PEc c) 1 nil
+  | FEX x => mk_linear (PEX C x) 1 nil
   | FEadd e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
       let s := split (denum x) (denum y) in
       mk_linear
-        (NPEadd (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
-        (NPEmul (left s) (NPEmul (right s) (common s)))
-        (condition x ++ condition y)
-
+        ((num x ** right s) ++ (num y ** left s))
+        (left s ** (right s ** common s))
+        (condition x ++ condition y)%list
   | FEsub e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
       let s := split (denum x) (denum y) in
       mk_linear
-        (NPEsub (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
-        (NPEmul (left s) (NPEmul (right s) (common s)))
-        (condition x ++ condition y)
+        ((num x ** right s) -- (num y ** left s))
+        (left s ** (right s ** common s))
+        (condition x ++ condition y)%list
   | FEmul e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
       let s1 := split (num x) (denum y) in
       let s2 := split (num y) (denum x) in
-      mk_linear (NPEmul (left s1) (left s2))
-        (NPEmul (right s2) (right s1))
-        (condition x ++ condition y)
+      mk_linear (left s1 ** left s2)
+        (right s2 ** right s1)
+        (condition x ++ condition y)%list
   | FEopp e1 =>
       let x := Fnorm e1 in
       mk_linear (NPEopp (num x)) (denum x) (condition x)
@@ -978,15 +1071,14 @@ Fixpoint Fnorm (e : FExpr) : linear :=
       let y := Fnorm e2 in
       let s1 := split (num x) (num y) in
       let s2 := split (denum x) (denum y) in
-      mk_linear (NPEmul (left s1) (right s2))
-        (NPEmul (left s2) (right s1))
-        (num y :: condition x ++ condition y)
+      mk_linear (left s1 ** right s2)
+        (left s2 ** right s1)
+        (num y :: condition x ++ condition y)%list
   | FEpow e1 n =>
       let x := Fnorm e1 in
-      mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x)
+      mk_linear ((num x)^^n) ((denum x)^^n) (condition x)
   end.
 
-
 (* Example *)
 (*
 Eval compute
@@ -996,93 +1088,31 @@ Eval compute
           (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))).
 *)
 
- Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0.
+Theorem Pcond_Fnorm l e :
+ PCond l (condition (Fnorm e)) ->  ~ (denum (Fnorm e))@l == 0.
 Proof.
- induction p;simpl.
-  intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
-  apply IHp.
-  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  reflexivity.
-  rewrite H1. ring. rewrite Hp;ring.
-  intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  reflexivity. rewrite Hp;ring. trivial.
-Qed.
-
-Theorem Pcond_Fnorm:
- forall l e,
- PCond l (condition (Fnorm e)) ->  ~ NPEeval l (denum (Fnorm e)) == 0.
-intros l e; elim e.
- simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
- simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-   intros HH; case Hrec1; auto.
-     apply PCond_app_inv_l with (1 := Hcond).
-   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-   rewrite NPEmul_correct; simpl; rewrite HH; ring.
-   intros HH; case Hrec2; auto.
-     apply PCond_app_inv_r with (1 := Hcond).
-   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-   intros HH; case Hrec1; auto.
-     apply PCond_app_inv_l with (1 := Hcond).
-   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-   rewrite NPEmul_correct; simpl; rewrite HH; ring.
-   intros HH; case Hrec2; auto.
-     apply PCond_app_inv_r with (1 := Hcond).
-   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-  intros HH; apply Hrec1.
-    apply PCond_app_inv_l with (1 := Hcond).
-    rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
-  intros HH; apply Hrec2.
-    apply PCond_app_inv_r with (1 := Hcond).
-    rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
- intros e1 Hrec1 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   auto.
- intros e1 Hrec1 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   apply PCond_cons_inv_l with (1:=Hcond).
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl condition in Hcond.
-   simpl denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-    intros HH; apply Hrec1.
-    specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
-    apply PCond_app_inv_l with (1 := Hcond1).
-    rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
-    intros HH; apply PCond_cons_inv_l with (1:=Hcond).
-    rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
- simpl;intros e1 Hrec1 n Hcond.
-  rewrite NPEpow_correct.
-  simpl;rewrite pow_th.(rpow_pow_N).
-  destruct n;simpl;intros.
-  apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto.
-Qed.
-Hint Resolve Pcond_Fnorm.
+induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
+ simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
+- simpl. rewrite phi_1; exact rI_neq_rO.
+- simpl. rewrite phi_1; exact rI_neq_rO.
+- simpl; intros. rewrite phi_1; exact rI_neq_rO.
+- simpl; intros. rewrite phi_1; exact rI_neq_rO.
+- rewrite <- split_ok_r. simpl. apply field_is_integral_domain.
+  + apply split_nz_l, IHe1, Hc1.
+  + apply IHe2, Hc2.
+- rewrite <- split_ok_r. simpl. apply field_is_integral_domain.
+  + apply split_nz_l, IHe1, Hc1.
+  + apply IHe2, Hc2.
+- simpl. apply field_is_integral_domain.
+  + apply split_nz_r, IHe1, Hc1.
+  + apply split_nz_r, IHe2, Hc2.
+- now apply IHe.
+- trivial.
+- destruct Hc2 as (Hc2,_). simpl. apply field_is_integral_domain.
+  + apply split_nz_l, IHe1, Hc2.
+  + apply split_nz_r, Hc1.
+- rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc.
+Qed.
 
 
 (***************************************************************************
@@ -1091,154 +1121,106 @@ Hint Resolve Pcond_Fnorm.
 
   ***************************************************************************)
 
-Theorem Fnorm_FEeval_PEeval:
- forall l fe,
+Ltac uneval :=
+ repeat match goal with
+  | |- context [ ?x @ ?l * ?y @ ?l ] => change (x@l * y@l) with ((x*y)@l)
+  | |- context [ ?x @ ?l + ?y @ ?l ] => change (x@l + y@l) with ((x+y)@l)
+ end.
+
+Theorem Fnorm_FEeval_PEeval l fe:
  PCond l (condition (Fnorm fe)) ->
- FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)).
-Proof.
-intros l fe; elim fe; simpl.
-intros c H; rewrite CRmorph.(morph1); apply rdiv1.
-intros p H; rewrite CRmorph.(morph1); apply rdiv1.
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-rewrite NPEadd_correct; simpl.
-repeat rewrite NPEmul_correct; simpl.
-generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2; rewrite U1; rewrite U2.
-apply rdiv2b; auto.
-  rewrite <- U1; auto.
-  rewrite <- U2; auto.
-
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-rewrite NPEsub_correct; simpl.
-repeat rewrite NPEmul_correct; simpl.
-generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2; rewrite U1; rewrite U2.
-apply rdiv3b; auto.
-  rewrite <- U1; auto.
-  rewrite <- U2; auto.
-
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-repeat rewrite NPEmul_correct; simpl.
-generalize (split_correct_l l (num (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_l l (num (Fnorm e2)) (denum (Fnorm e1)))
-   (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
-  rewrite U4; simpl.
-apply rdiv4b; auto.
-  rewrite <- U4; auto.
-  rewrite <- U2; auto.
-
-intros e1 He1 HH.
-rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto.
-
-intros e1 He1 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_cons_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); apply rdiv6; auto.
-apply PCond_cons_inv_l with ( 1 := HH ).
-
-intros e1 He1 e2 He2 HH.
-assert (HH1: PCond l (condition (Fnorm e1))).
-apply PCond_app_inv_l with (condition (Fnorm e2)).
-apply PCond_cons_inv_r with ( 1 := HH ).
-assert (HH2: PCond l (condition (Fnorm e2))).
-apply PCond_app_inv_r with (condition (Fnorm e1)).
-apply PCond_cons_inv_r with ( 1 := HH ).
-rewrite (He1 HH1); rewrite (He2 HH2).
-repeat rewrite NPEmul_correct;simpl.
-generalize (split_correct_l l (num (Fnorm e1)) (num (Fnorm e2)))
-   (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2)))
-   (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
-   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
-repeat rewrite NPEmul_correct; simpl.
-intros U1 U2 U3 U4; rewrite U1; rewrite U2; rewrite U3;
-  rewrite U4; simpl.
-apply rdiv7b; auto.
-  rewrite <- U3; auto.
-  rewrite <- U2; auto.
-apply PCond_cons_inv_l with ( 1 := HH ).
-  rewrite <- U4; auto.
-
-intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1.
-repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N).
-rewrite He1';clear He1'.
-destruct n;simpl. apply rdiv1.
-generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1)))
-  (Pcond_Fnorm _ _ Hcond).
-intros r r0 Hdiff;induction p;simpl.
-repeat (rewrite <- rdiv4;trivial).
-rewrite IHp. reflexivity.
-apply pow_pos_not_0;trivial.
-apply pow_pos_not_0;trivial.
-intro Hp. apply (pow_pos_not_0 Hdiff  p).
-rewrite  (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p)  0).
- reflexivity. apply pow_pos_not_0;trivial. ring [Hp].
-rewrite <- rdiv4;trivial.
-rewrite IHp;reflexivity.
-apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
-reflexivity.
-Qed.
-
-Theorem Fnorm_crossproduct:
- forall l fe1 fe2,
+ FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l.
+Proof.
+induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
+ intros (Hc1,Hc2) || intros Hc;
+ try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1);
+ try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2);
+ try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *.
+
+- now rewrite phi_1, phi_0, rdiv_def.
+- now rewrite phi_1; apply rdiv1.
+- rewrite phi_1; apply rdiv1.
+- rewrite phi_1; apply rdiv1.
+- rewrite NPEadd_ok, !NPEmul_ok. simpl.
+  rewrite <- rdiv2b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial.
+  now f_equiv.
+
+- rewrite NPEsub_ok, !NPEmul_ok. simpl.
+  rewrite <- rdiv3b; uneval; rewrite <- ?split_ok_l, <- ?split_ok_r; trivial.
+  now f_equiv.
+
+- rewrite !NPEmul_ok. simpl.
+  rewrite IHfe1, IHfe2.
+  rewrite (split_ok_l (num F1) (denum F2) l),
+          (split_ok_r (num F1) (denum F2) l),
+          (split_ok_l (num F2) (denum F1) l),
+          (split_ok_r (num F2) (denum F1) l) in *.
+  apply rdiv4b; trivial.
+
+- rewrite NPEopp_ok; simpl; rewrite (IHfe Hc); apply rdiv5.
+
+- rewrite (IHfe Hc2); apply rdiv6; trivial;
+   apply Pcond_Fnorm; trivial.
+
+- destruct Hc2 as (Hc2,Hc3).
+  rewrite !NPEmul_ok. simpl.
+  assert (U1 := split_ok_l (num F1) (num F2) l).
+  assert (U2 := split_ok_r (num F1) (num F2) l).
+  assert (U3 := split_ok_l (denum F1) (denum F2) l).
+  assert (U4 := split_ok_r (denum F1) (denum F2) l).
+  rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4.
+  simpl in U2, U3, U4. apply rdiv7b;
+   rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial.
+
+- rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc).
+  destruct n; simpl.
+  + apply rdiv1.
+  + apply pow_pos_div. apply Pcond_Fnorm; trivial.
+Qed.
+
+Theorem Fnorm_crossproduct l fe1 fe2 :
  let nfe1 := Fnorm fe1 in
  let nfe2 := Fnorm fe2 in
- NPEeval l (PEmul (num nfe1) (denum nfe2)) ==
- NPEeval l (PEmul (num nfe2) (denum nfe1)) ->
+ (num nfe1 * denum nfe2) @ l == (num nfe2 * denum nfe1) @ l ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
-intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
-rewrite Fnorm_FEeval_PEeval by
- apply PCond_app_inv_l with (1 := Hcond).
- rewrite Fnorm_FEeval_PEeval by
-  apply PCond_app_inv_r with (1 := Hcond).
-  apply cross_product_eq; trivial.
-   apply Pcond_Fnorm.
-     apply PCond_app_inv_l with (1 := Hcond).
-   apply Pcond_Fnorm.
-     apply PCond_app_inv_r with (1 := Hcond).
+Proof.
+simpl. rewrite PCond_app. intros Hcrossprod (Hc1,Hc2).
+rewrite !Fnorm_FEeval_PEeval; trivial.
+apply cross_product_eq; trivial;
+ apply Pcond_Fnorm; trivial.
 Qed.
 
 (* Correctness lemmas of reflexive tactics *)
-Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow).
-Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
+Notation Ninterp_PElist :=
+  (interp_PElist rO rI radd rmul rsub ropp req phi Cp_phi rpow).
+Notation Nmk_monpol_list :=
+  (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
 
-Theorem Fnorm_correct:
+Theorem Fnorm_ok:
  forall n l lpe fe,
   Ninterp_PElist l lpe ->
   Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true ->
   PCond l (condition (Fnorm fe)) ->  FEeval l fe == 0.
-intros n l lpe fe Hlpe H H1;
- apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1).
-apply rdiv8; auto.
-transitivity (NPEeval l (PEc cO)); auto.
-rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe);auto.
-change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)).
-apply (Peq_ok Rsth Reqe CRmorph);auto.
-simpl. apply (morph0 CRmorph); auto.
+Proof.
+intros n l lpe fe Hlpe H H1.
+rewrite (Fnorm_FEeval_PEeval l fe H1).
+apply rdiv8. apply Pcond_Fnorm; trivial.
+transitivity (0@l); trivial.
+rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th cdiv_th n l lpe); trivial.
+change (0 @ l) with (Pphi 0 radd rmul phi l (Pc cO)).
+apply (Peq_ok Rsth Reqe CRmorph); trivial.
 Qed.
 
+Notation ring_rw_correct :=
+ (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
+
+Notation ring_rw_pow_correct :=
+ (ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
+
+Notation ring_correct :=
+ (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th).
+
 (* simplify a field expression into a fraction *)
 (* TODO: simplify when den is constant... *)
 Definition display_linear l num den :=
@@ -1247,71 +1229,54 @@ Definition display_linear l num den :=
 Definition display_pow_linear l num den :=
   NPphi_pow l num / NPphi_pow l den.
 
-Theorem Field_rw_correct :
- forall n lpe l,
+Theorem Field_rw_correct n lpe l :
    Ninterp_PElist l lpe ->
    forall lmp, Nmk_monpol_list lpe = lmp ->
    forall fe nfe, Fnorm fe = nfe ->
    PCond l (condition nfe) ->
-   FEeval l fe == display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
+   FEeval l fe ==
+     display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
 Proof.
-  intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
-  apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
-  unfold display_linear; apply SRdiv_ext;
-  eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto.
+  intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
+  rewrite (Fnorm_FEeval_PEeval _ _ H).
+  unfold display_linear; apply rdiv_ext;
+  eapply ring_rw_correct; eauto.
 Qed.
 
-Theorem Field_rw_pow_correct :
- forall n lpe l,
+Theorem Field_rw_pow_correct n lpe l :
    Ninterp_PElist l lpe ->
    forall lmp, Nmk_monpol_list lpe = lmp ->
    forall fe nfe, Fnorm fe = nfe ->
    PCond l (condition nfe) ->
-   FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
+   FEeval l fe ==
+     display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)).
 Proof.
-  intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
-  apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
-  unfold display_pow_linear; apply SRdiv_ext;
-  eapply (ring_rw_pow_correct Rsth Reqe ARth CRmorph);eauto.
+  intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp.
+  rewrite (Fnorm_FEeval_PEeval _ _ H).
+  unfold display_pow_linear; apply rdiv_ext;
+  eapply ring_rw_pow_correct;eauto.
 Qed.
 
-Theorem Field_correct :
- forall n l lpe fe1 fe2, Ninterp_PElist l lpe ->
+Theorem Field_correct n l lpe fe1 fe2 :
+ Ninterp_PElist l lpe ->
  forall lmp, Nmk_monpol_list lpe = lmp ->
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
- Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2)))
-          (Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true ->
+ Peq ceqb (Nnorm n lmp (num nfe1 * denum nfe2))
+          (Nnorm n lmp (num nfe2 * denum nfe1)) = true ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
+intros Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
 apply Fnorm_crossproduct; trivial.
-eapply (ring_correct Rsth Reqe ARth CRmorph); eauto.
+eapply ring_correct; eauto.
 Qed.
 
 (* simplify a field equation : generate the crossproduct and simplify
    polynomials *)
-Theorem Field_simplify_eq_old_correct :
- forall l fe1 fe2 nfe1 nfe2,
- Fnorm fe1 = nfe1 ->
- Fnorm fe2 = nfe2 ->
- NPphi_dev l (Nnorm O nil (PEmul (num nfe1) (denum nfe2))) ==
- NPphi_dev l (Nnorm O nil (PEmul (num nfe2) (denum nfe1))) ->
- PCond l (condition nfe1 ++ condition nfe2) ->
- FEeval l fe1 == FEeval l fe2.
-Proof.
-intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond;  subst nfe1 nfe2.
-apply Fnorm_crossproduct; trivial.
-match goal with
- [ |- NPEeval l ?x == NPEeval l ?y] =>
-    rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
-       O nil l I Logic.eq_refl x Logic.eq_refl);
-    rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec
-       O nil l I Logic.eq_refl y Logic.eq_refl)
- end.
-trivial.
-Qed.
+
+(** This allows rewriting modulo the simplification of PEeval on PMul *)
+Declare Equivalent Keys PEeval rmul.
 
 Theorem Field_simplify_eq_correct :
  forall n l lpe fe1 fe2,
@@ -1320,37 +1285,23 @@ Theorem Field_simplify_eq_correct :
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
- NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
+ NPphi_dev l (Nnorm n lmp (num nfe1 * right den)) ==
+ NPphi_dev l (Nnorm n lmp (num nfe2 * left den)) ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
-  subst nfe1 nfe2 den lmp.
-apply Fnorm_crossproduct; trivial.
+intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond.
+apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial.
 simpl.
-rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite NPEmul_correct.
-rewrite NPEmul_correct.
+rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3.
+rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
 simpl.
-repeat rewrite (ARmul_assoc ARth).
-rewrite <-(
-  let x := PEmul (num (Fnorm fe1))
-                     (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
-ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-rewrite <-(
-  let x := (PEmul (num (Fnorm fe2))
-                     (rsplit_left
-                        (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
-    ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-simpl in Hcrossprod.
-rewrite Hcrossprod.
-reflexivity.
+rewrite !rmul_assoc.
+apply rmul_ext; trivial.
+rewrite (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
+ (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
+rewrite Hlmp.
+apply Hcrossprod.
 Qed.
 
 Theorem Field_simplify_eq_pow_correct :
@@ -1360,37 +1311,55 @@ Theorem Field_simplify_eq_pow_correct :
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
- NPphi_pow l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
+ NPphi_pow l (Nnorm n lmp (num nfe1 * right den)) ==
+ NPphi_pow l (Nnorm n lmp (num nfe2 * left den)) ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
-  subst nfe1 nfe2 den lmp.
-apply Fnorm_crossproduct; trivial.
+intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond.
+apply Fnorm_crossproduct; rewrite ?eq1, ?eq2; trivial.
 simpl.
-rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
-rewrite NPEmul_correct.
-rewrite NPEmul_correct.
+rewrite (split_ok_l (denum nfe1) (denum nfe2) l), eq3.
+rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
 simpl.
-repeat rewrite (ARmul_assoc ARth).
-rewrite <-(
-  let x := PEmul (num (Fnorm fe1))
-                     (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in
-ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-rewrite <-(
-  let x := (PEmul (num (Fnorm fe2))
-                     (rsplit_left
-                        (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in
-    ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec n lpe l
-        Hlpe Logic.eq_refl
-        x Logic.eq_refl) in Hcrossprod.
-simpl in Hcrossprod.
-rewrite Hcrossprod.
-reflexivity.
+rewrite !rmul_assoc.
+apply rmul_ext; trivial.
+rewrite
+ (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
+ (ring_rw_pow_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
+rewrite Hlmp.
+apply Hcrossprod.
+Qed.
+
+Theorem Field_simplify_aux_ok l fe1 fe2 den :
+ FEeval l fe1 == FEeval l fe2 ->
+ split (denum (Fnorm fe1)) (denum (Fnorm fe2)) = den ->
+ PCond l (condition (Fnorm fe1) ++ condition (Fnorm fe2)) ->
+ (num (Fnorm fe1) * right den) @ l == (num (Fnorm fe2) * left den) @ l.
+Proof.
+ rewrite PCond_app; intros Hfe Hden (Hc1,Hc2); simpl.
+ assert (Hc1' := Pcond_Fnorm _ _ Hc1).
+ assert (Hc2' := Pcond_Fnorm _ _ Hc2).
+ set (N1 := num (Fnorm fe1)) in *. set (N2 := num (Fnorm fe2)) in *.
+ set (D1 := denum (Fnorm fe1)) in *. set (D2 := denum (Fnorm fe2)) in *.
+ assert (~ (common den) @ l == 0).
+ { intro H. apply Hc1'.
+   rewrite (split_ok_l D1 D2 l).
+   rewrite Hden. simpl. ring [H]. }
+ apply (@rmul_reg_l ((common den) @ l)); trivial.
+ rewrite !(rmul_comm ((common den) @ l)), <- !rmul_assoc.
+ change
+  (N1@l * (right den * common den) @ l ==
+   N2@l * (left den * common den) @ l).
+ rewrite <- Hden, <- split_ok_l, <- split_ok_r.
+ apply (@rmul_reg_l (/ D2@l)). { apply rinv_nz; trivial. }
+ rewrite (rmul_comm (/ D2 @ l)), <- !rmul_assoc.
+ rewrite <- rdiv_def, rdiv_r_r, rmul_1_r by trivial.
+ apply (@rmul_reg_l (/ (D1@l))). { apply rinv_nz; trivial. }
+ rewrite !(rmul_comm  (/ D1@l)), <- !rmul_assoc.
+ rewrite <- !rdiv_def, rdiv_r_r, rmul_1_r by trivial.
+ rewrite (rmul_comm (/ D2@l)), <- rdiv_def.
+ unfold N1,N2,D1,D2; rewrite <- !Fnorm_FEeval_PEeval; trivial.
 Qed.
 
 Theorem Field_simplify_eq_pow_in_correct :
@@ -1400,47 +1369,17 @@ Theorem Field_simplify_eq_pow_in_correct :
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 ->
- forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 ->
+ forall np1, Nnorm n lmp (num nfe1 * right den) = np1 ->
+ forall np2, Nnorm n lmp (num nfe2 * left den) = np2 ->
  FEeval l fe1 == FEeval l fe2 ->
-  PCond l (condition nfe1 ++ condition nfe2) ->
+ PCond l (condition nfe1 ++ condition nfe2) ->
  NPphi_pow l np1 ==
  NPphi_pow l np2.
 Proof.
  intros. subst nfe1 nfe2 lmp np1 np2.
- repeat rewrite (Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
- repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl.
- assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)).
- assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)).
- apply (@rmul_reg_l (NPEeval l (rsplit_common den))).
- intro Heq;apply N1.
- rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
- rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq].
- repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))).
- repeat rewrite <- ARth.(ARmul_assoc).
- change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))).
- change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))).
- repeat rewrite <- NPEmul_correct. rewrite <- H3. rewrite <- split_correct_l.
- rewrite <- split_correct_r.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
- ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
- ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
- rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval ; trivial.
- apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
+ rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
+ repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
+ simpl. apply Field_simplify_aux_ok; trivial.
 Qed.
 
 Theorem Field_simplify_eq_in_correct :
@@ -1450,47 +1389,16 @@ forall n l lpe fe1 fe2,
  forall nfe1, Fnorm fe1 = nfe1 ->
  forall nfe2, Fnorm fe2 = nfe2 ->
  forall den, split (denum nfe1) (denum nfe2) = den ->
- forall np1, Nnorm n lmp (PEmul (num nfe1) (right den)) = np1 ->
- forall np2, Nnorm n lmp (PEmul (num nfe2) (left den)) = np2 ->
+ forall np1, Nnorm n lmp (num nfe1 * right den) = np1 ->
+ forall np2, Nnorm n lmp (num nfe2 * left den) = np2 ->
  FEeval l fe1 == FEeval l fe2 ->
-  PCond l (condition nfe1 ++ condition nfe2) ->
- NPphi_dev l np1 ==
- NPphi_dev l np2.
+ PCond l (condition nfe1 ++ condition nfe2) ->
+ NPphi_dev l np1 == NPphi_dev l np2.
 Proof.
  intros. subst nfe1 nfe2 lmp np1 np2.
- repeat rewrite (Pphi_dev_ok Rsth Reqe ARth CRmorph  get_sign_spec).
- repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl.
- assert (N1 := Pcond_Fnorm _ _ (PCond_app_inv_l _ _ _ H7)).
- assert (N2 := Pcond_Fnorm _ _ (PCond_app_inv_r _ _ _ H7)).
- apply (@rmul_reg_l (NPEeval l (rsplit_common den))).
- intro Heq;apply N1.
- rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))).
- rewrite H3. rewrite NPEmul_correct. simpl. ring [Heq].
- repeat rewrite (ARth.(ARmul_comm) (NPEeval l (rsplit_common den))).
- repeat rewrite <- ARth.(ARmul_assoc).
- change (NPEeval l (rsplit_right den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_right den) (rsplit_common den))).
- change (NPEeval l (rsplit_left den) * NPEeval l (rsplit_common den)) with
-      (NPEeval l (PEmul (rsplit_left den) (rsplit_common den))).
- repeat rewrite <- NPEmul_correct;rewrite <- H3. rewrite <- split_correct_l.
- rewrite <- split_correct_r.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe2)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
- ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
- intro Heq; apply AFth.(AF_1_neq_0).
- rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
- ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
- repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
- rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
- rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
- repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
+ rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph  get_sign_spec).
+ repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
+ apply Field_simplify_aux_ok; trivial.
 Qed.
 
 
@@ -1499,7 +1407,7 @@ Section Fcons_impl.
 Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C).
 
 Hypothesis PCond_fcons_inv : forall l a l1,
-  PCond l (Fcons a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
+  PCond l (Fcons a l1) ->  ~ a @ l == 0 /\ PCond l l1.
 
 Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   match l with
@@ -1507,15 +1415,15 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   | cons a l1 => Fcons a (Fapp l1 m)
   end.
 
- Lemma fcons_correct : forall l l1,
+Lemma fcons_ok : forall l l1,
   (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
- Proof.
- intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
- induction l1; simpl; intros.
-  trivial.
-  elim PCond_fcons_inv with (1 := H); intros.
-  destruct l1; trivial. split; trivial. apply IHl1; trivial.
- Qed.
+Proof.
+intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
+induction l1; simpl; intros.
+ trivial.
+ elim PCond_fcons_inv with (1 := H); intros.
+ destruct l1; trivial. split; trivial. apply IHl1; trivial.
+Qed.
 
 End Fcons_impl.
 
@@ -1531,21 +1439,15 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
  end.
 
 Theorem PFcons_fcons_inv:
- forall l a l1, PCond l (Fcons a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a l1; elim l1; simpl Fcons; auto.
-simpl; auto.
-intros a0 l0.
-generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0).
-intros H H0 H1; split; auto.
-rewrite H; auto.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-intros H H0 H1;
- assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
-split.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-apply H0.
-generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
-generalize Hp; case l0; simpl; intuition.
+ forall l a l1, PCond l (Fcons a l1) ->  ~ a @ l == 0 /\ PCond l l1.
+Proof.
+induction l1 as [|e l1]; simpl Fcons.
+- simpl; now split.
+- case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2);
+   repeat split; trivial.
+  + now rewrite H.
+  + now apply IHl1.
+  + now apply IHl1.
 Qed.
 
 (* equality of normal forms rather than syntactic equality *)
@@ -1558,23 +1460,16 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
  end.
 
 Theorem PFcons0_fcons_inv:
- forall l a l1, PCond l (Fcons0 a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a l1; elim l1; simpl Fcons0; auto.
-simpl; auto.
-intros a0 l0.
-generalize (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th O l nil a a0). simpl.
-  case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)).
-intros H H0 H1; split; auto.
-rewrite H; auto.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-intros H H0 H1;
- assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
-split.
-generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
-apply H0.
-generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
-clear get_sign get_sign_spec.
-generalize Hp; case l0; simpl; intuition.
+ forall l a l1, PCond l (Fcons0 a l1) ->  ~ a @ l == 0 /\ PCond l l1.
+Proof.
+induction l1 as [|e l1]; simpl Fcons0.
+- simpl; now split.
+- generalize (ring_correct O l nil a e). lazy zeta; simpl Peq.
+  case Peq; intros H; rewrite !PCond_cons; intros (H1,H2);
+   repeat split; trivial.
+  + now rewrite H.
+  + now apply IHl1.
+  + now apply IHl1.
 Qed.
 
 (* split factorized denominators *)
@@ -1586,95 +1481,83 @@ Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
  end.
 
 Theorem PFcons00_fcons_inv:
-  forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
- intros p H p0 H0 l1 H1.
-   simpl in H1.
-   case (H _ H1); intros H2 H3.
-   case (H0 _ H3); intros H4 H5; split; auto.
-   simpl.
-   apply field_is_integral_domain; trivial.
-   simpl;intros. rewrite pow_th.(rpow_pow_N).
-   destruct (H _ H0);split;auto.
-   destruct n;simpl. apply AFth.(AF_1_neq_0).
-   apply pow_pos_not_0;trivial.
+  forall l a l1, PCond l (Fcons00 a l1) -> ~ a @ l == 0 /\ PCond l l1.
+Proof.
+intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
+- intros p H p0 H0 l1 H1.
+  simpl in H1.
+  destruct (H _ H1) as (H2,H3).
+  destruct (H0 _ H3) as (H4,H5). split; trivial.
+  simpl.
+  apply field_is_integral_domain; trivial.
+- intros. destruct (H _ H0). split; trivial.
+  apply PEpow_nz; trivial.
 Qed.
 
 Definition Pcond_simpl_gen :=
-  fcons_correct _ PFcons00_fcons_inv.
+  fcons_ok _ PFcons00_fcons_inv.
 
 
 (* Specific case when the equality test of coefs is complete w.r.t. the
    field equality: non-zero coefs can be eliminated, and opposite can
    be simplified (if -1 <> 0) *)
 
-Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true.
+Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true.
 
-Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
-  (phi c1 == phi c2 -> P x) ->
-  (~ phi c1 == phi c2 -> P y) ->
-  P (if ceqb c1 c2 then x else y).
+Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2).
 Proof.
-intros.
-generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
-generalize (@ceqb_complete c1 c2).
-case (c1 ?=! c2); auto; intros.
-apply X0.
-red; intro.
-absurd (false = true); auto;  discriminate.
+assert (H := morph_eq CRmorph c1 c2).
+assert (H' := @ceqb_complete c1 c2).
+destruct (ceqb c1 c2); constructor.
+- now apply H.
+- intro E. specialize (H' E). discriminate.
 Qed.
 
 Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
  match e with
-   PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l)
+ | PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l)
  | PEpow e _ => Fcons1 e l
- | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l
- | PEc c => if ceqb c cO then absurd_PCond else l
+ | PEopp e => if (-(1) =? 0)%coef then absurd_PCond else Fcons1 e l
+ | PEc c => if (c =? 0)%coef then absurd_PCond else l
  | _ => Fcons0 e l
  end.
 
 Theorem PFcons1_fcons_inv:
-  forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
-intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
- simpl; intros c l1.
-   apply ceqb_rect_complete; intros.
-  elim (@absurd_PCond_bottom l H0).
-  split; trivial.
-    rewrite <- (morph0 CRmorph); trivial.
- intros p H p0 H0 l1 H1.
-   simpl in H1.
-   case (H _ H1); intros H2 H3.
-   case (H0 _ H3); intros H4 H5; split; auto.
-   simpl.
-   apply field_is_integral_domain; trivial.
- simpl; intros p H l1.
-   apply ceqb_rect_complete; intros.
-  elim (@absurd_PCond_bottom l H1).
-  destruct (H _ H1).
+  forall l a l1, PCond l (Fcons1 a l1) -> ~ a @ l == 0 /\ PCond l l1.
+Proof.
+intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
+- simpl; intros c l1.
+  case ceqb_spec'; intros H H0.
+  + elim (@absurd_PCond_bottom l H0).
+  + split; trivial. rewrite <- phi_0; trivial.
+- intros p H p0 H0 l1 H1. simpl in H1.
+  destruct (H _ H1) as (H2,H3).
+  destruct (H0 _ H3) as (H4,H5).
+  split; trivial. simpl. apply field_is_integral_domain; trivial.
+- simpl; intros p H l1.
+  case ceqb_spec'; intros H0 H1.
+  + elim (@absurd_PCond_bottom l H1).
+  + destruct (H _ H1).
     split; trivial.
     apply ropp_neq_0; trivial.
-    rewrite (morph_opp CRmorph) in H0.
-    rewrite (morph1 CRmorph) in H0.
-    rewrite (morph0 CRmorph) in H0.
-    trivial.
- intros;simpl. destruct (H _ H0);split;trivial.
- rewrite pow_th.(rpow_pow_N). destruct n;simpl.
- apply AFth.(AF_1_neq_0). apply pow_pos_not_0;trivial.
+    rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial.
+- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial.
 Qed.
 
-Definition Fcons2 e l := Fcons1 (PExpr_simp e) l.
+Definition Fcons2 e l := Fcons1 (PEsimp e) l.
 
 Theorem PFcons2_fcons_inv:
- forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
+ forall l a l1, PCond l (Fcons2 a l1) -> ~ a @ l == 0 /\ PCond l l1.
+Proof.
 unfold Fcons2; intros l a l1 H; split;
- case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto.
+ case (PFcons1_fcons_inv l (PEsimp a) l1); trivial.
 intros H1 H2 H3; case H1.
-transitivity (NPEeval l a); trivial.
-apply PExpr_simp_correct.
+transitivity (a@l); trivial.
+apply PEsimp_ok.
 Qed.
 
 Definition Pcond_simpl_complete :=
-  fcons_correct _ PFcons2_fcons_inv.
+  fcons_ok _ PFcons2_fcons_inv.
 
 End Fcons_simpl.
 
@@ -1742,22 +1625,22 @@ Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
 
 Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
 
-Lemma add_inj_r : forall p x y,
+Lemma add_inj_r p x y :
    gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
-intros p x y.
+Proof.
 elim p using Pos.peano_ind; simpl; intros.
  apply S_inj; trivial.
  apply H.
    apply S_inj.
-   repeat rewrite (ARadd_assoc ARth).
+   rewrite !(ARadd_assoc ARth).
    rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth); trivial.
 Qed.
 
-Lemma gen_phiPOS_inj : forall x y,
+Lemma gen_phiPOS_inj x y :
   gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
   x = y.
-intros x y.
-repeat rewrite <- (same_gen Rsth Reqe ARth).
+Proof.
+rewrite <- !(same_gen Rsth Reqe ARth).
 case (Pos.compare_spec x y).
  intros.
    trivial.
@@ -1777,9 +1660,10 @@ case (Pos.compare_spec x y).
 Qed.
 
 
-Lemma gen_phiN_inj : forall x y,
+Lemma gen_phiN_inj x y :
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
   x = y.
+Proof.
 destruct x; destruct y; simpl; intros; trivial.
  elim gen_phiPOS_not_0 with p.
    symmetry .
@@ -1789,7 +1673,7 @@ destruct x; destruct y; simpl; intros; trivial.
  rewrite gen_phiPOS_inj with (1 := H); trivial.
 Qed.
 
-Lemma gen_phiN_complete : forall x y,
+Lemma gen_phiN_complete x y :
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
   N.eqb x y = true.
 Proof.
@@ -1808,31 +1692,22 @@ Section Field.
  Let AFth := F2AF Rsth Reqe Fth.
  Let ARth := Rth_ARth Rsth Reqe Rth.
 
-Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
+Lemma ring_S_inj x y : 1+x==1+y -> x==y.
+Proof.
 intros.
-transitivity (x + (1 + - (1))).
- rewrite (Ropp_def Rth).
-   symmetry .
-   apply (ARadd_0_r Rsth ARth).
- transitivity (y + (1 + - (1))).
-  repeat rewrite <- (ARplus_assoc ARth).
-    repeat rewrite (ARadd_assoc ARth).
-    apply (Radd_ext Reqe).
-   repeat rewrite <- (ARadd_comm ARth 1).
-     trivial.
-   reflexivity.
-  rewrite (Ropp_def Rth).
-    apply (ARadd_0_r Rsth ARth).
+rewrite <- (ARadd_0_l ARth x), <- (ARadd_0_l ARth y).
+rewrite <- (Ropp_def Rth 1), (ARadd_comm ARth 1).
+rewrite <- !(ARadd_assoc ARth). now apply (Radd_ext Reqe).
 Qed.
 
-
- Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
+Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
 
 Let gen_phiPOS_inject :=
    gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
 
-Lemma gen_phiPOS_discr_sgn : forall x y,
+Lemma gen_phiPOS_discr_sgn x y :
   ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
+Proof.
 red; intros.
 apply gen_phiPOS_not_0 with (y + x)%positive.
 rewrite (ARgen_phiPOS_add Rsth Reqe ARth).
@@ -1845,9 +1720,10 @@ transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
  apply (Ropp_def Rth).
 Qed.
 
-Lemma gen_phiZ_inj : forall x y,
+Lemma gen_phiZ_inj x y :
   gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
   x = y.
+Proof.
 destruct x; destruct y; simpl; intros.
  trivial.
  elim gen_phiPOS_not_0 with p.
@@ -1878,9 +1754,10 @@ destruct x; destruct y; simpl; intros.
    reflexivity.
 Qed.
 
-Lemma gen_phiZ_complete : forall x y,
+Lemma gen_phiZ_complete x y :
   gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
   Zeq_bool x y = true.
+Proof.
 intros.
  replace y with x.
  unfold Zeq_bool.
@@ -1891,3 +1768,6 @@ Qed.
 End Field.
 
 End Complete.
+
+Arguments FEO [C].
+Arguments FEI [C].
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index e106d5b5..b92b847b 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -1,13 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith_base.
-Require Import Zpow_def.
+Require Import Zbool.
 Require Import BinInt.
 Require Import BinNat.
 Require Import Setoid.
@@ -16,6 +15,7 @@ Require Import Ring_polynom.
 Import List.
 
 Set Implicit Arguments.
+(* Set Universe Polymorphism. *)
 
 Import RingSyntax.
 
@@ -815,7 +815,7 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
                   fun f => f arth ext_r morph lemma1 lemma2
                 | _ => fail 4 "ring: bad sign specification"
                 end
-             | _ => fail 3 "ring: bad coefficiant division specification"
+             | _ => fail 3 "ring: bad coefficient division specification"
              end
           | _ => fail 2 "ring: bad power specification"
           end
diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index cfd00521..a10eeecc 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v
index 95d7deee..2dc3197d 100644
--- a/plugins/setoid_ring/Ncring.v
+++ b/plugins/setoid_ring/Ncring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 516a993e..c40e0ffb 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -192,6 +192,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x].
  Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
  Proof. intros;subst;reflexivity. Qed.
 
+Declare Equivalent Keys bracket gen_phiZ.
 (*proof that [.] satisfies morphism specifications*)
 Global Instance gen_phiZ_morph :
 (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index eefc9428..5845b629 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -103,7 +103,7 @@ Variable P:Pol.
 
 (* Xi^n * P + Q
 les variables de tete de Q ne sont pas forcement < i 
-mais Q est normalisé : variables de tete decroissantes *)
+mais Q est normalisé : variables de tete decroissantes *)
 
 Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
   match Q with
@@ -216,8 +216,8 @@ Definition Psub(P P':Pol):= P ++ (--P').
   intros l P i n Q;unfold mkPX.
   destruct P;try (simpl;reflexivity).
   assert (Hh := ring_morphism_eq  c 0). 
-simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
-intros.
+  simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
+  intros.
   rewrite Hh. rewrite ring_morphism0.
   rsimpl. apply Ceqb_eq. trivial.
   destruct (Pos.compare_spec i p).
@@ -416,10 +416,13 @@ Qed.
  Variable pow_th : power_theory Cp_phi rpow.
 
  (** evaluation of polynomial expressions towards R *)
+
  Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
    match pe with
+   | PEO => 0
+   | PEI => 1
    | PEc c => [c]
-   | PEX j => nth 0 j l
+   | PEX _ j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
    | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
    | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
@@ -500,8 +503,10 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
 
   Fixpoint norm_aux (pe:PExpr C) : Pol :=
    match pe with
+   | PEO => Pc cO
+   | PEI => Pc cI
    | PEc c => Pc c
-   | PEX j => mk_X j
+   | PEX _ j => mk_X j
    | PEadd pe1 (PEopp pe2) =>
      Psub (norm_aux pe1) (norm_aux pe2)
    | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
@@ -520,28 +525,30 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
   Proof.
    intros.
    induction pe.
-Esimpl3. Esimpl3. simpl.
- rewrite IHpe1;rewrite IHpe2.
- destruct pe2; Esimpl3. 
-unfold Psub.
-destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
-simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
-destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity.
-Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
- Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
-simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
-simpl. rewrite IHpe; Esimpl3. 
-simpl.
-   rewrite Ppow_N_ok; (intros;try reflexivity). 
-   rewrite rpow_pow_N.  Esimpl3.
-   induction n;simpl. Esimpl3. induction p; simpl.
-  try rewrite IHp;try rewrite IHpe;
- repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;reflexivity.
-rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe;
- repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;reflexivity. trivial.
-exact pow_th.
+   - now simpl; rewrite <- ring_morphism0.
+   - now simpl; rewrite <- ring_morphism1.
+   - Esimpl3. 
+   - Esimpl3. 
+   - simpl.
+     rewrite IHpe1;rewrite IHpe2.
+     destruct pe2; Esimpl3. 
+     unfold Psub.
+     destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
+   - simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
+     now destruct pe1; 
+       [destruct pe2; rewrite Padd_ok; rewrite Popp_ok; Esimpl3 | Esimpl3..]. 
+   - simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
+   - now simpl; rewrite IHpe; Esimpl3. 
+   - simpl.
+     rewrite Ppow_N_ok; (intros;try reflexivity). 
+     rewrite rpow_pow_N; [| now apply pow_th]. 
+     induction n;simpl; [now Esimpl3|]. 
+     induction p; simpl; trivial.
+     + try rewrite IHp;try rewrite IHpe;
+         repeat rewrite Pms_ok; repeat rewrite Pmul_ok;reflexivity.
+     + rewrite Pmul_ok. 
+       try rewrite IHp;try rewrite IHpe; repeat rewrite Pms_ok;
+         repeat rewrite Pmul_ok;reflexivity. 
   Qed.
 
  Lemma norm_subst_spec :
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
index 4fb02909..31c9e54d 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -76,11 +76,11 @@ Instance  reify_mul (R:Type)
  : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
 
 Instance  reify_mul_ext (R:Type) `{Ring R}
-  lvar z e2 t2 
+  lvar (z:Z) e2 t2 
  `{Ring (T:=R)}
  {_:reify e2 lvar t2}
  : reify (PEmul (PEc z) e2) lvar
-      (@multiplication Z _ _  z t2)|9.
+      (@multiplication Z _ _ z t2)|9.
 
 Instance  reify_sub (R:Type)
  e1 lvar t1 e2 t2 op
@@ -127,7 +127,6 @@ Definition list_reifyl (R:Type) lexpr lvar lterm
 
 Unset Implicit Arguments.
 
-
 Ltac lterm_goal g :=
   match g with
   | ?t1 == ?t2 => constr:(t1::t2::nil)
@@ -138,6 +137,7 @@ Ltac lterm_goal g :=
 Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
  intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. 
 
+
 Ltac reify_goal lvar lexpr lterm:=
   (*idtac lvar; idtac lexpr; idtac lterm;*)
   match lexpr with
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index 98150d35..b2417db6 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index b64023ea..9508b8e7 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v
deleted file mode 100644
index 945f6c68..00000000
--- a/plugins/setoid_ring/Ring_equiv.v
+++ /dev/null
@@ -1,74 +0,0 @@
-Require Import Setoid_ring_theory.
-Require Import LegacyRing_theory.
-Require Import Ring_theory.
-
-Set Implicit Arguments.
-
-Section Old2New.
-
-Variable A : Type.
-
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aopp : A -> A.
-Variable Aeq : A -> A -> bool.
-Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
-
-Let Aminus := fun x y => Aplus x (Aopp y).
-
-Lemma ring_equiv1 :
-  ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
-Proof.
-destruct R.
-split;  eauto.
-Qed.
-
-End Old2New.
-
-Section New2OldRing.
- Variable R : Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
-
- Variable reqb : R -> R -> bool.
- Variable reqb_ok : forall x y, reqb x y = true -> x = y.
-
- Lemma ring_equiv2 :
-   Ring_Theory radd  rmul rI rO ropp reqb.
-Proof.
-elim Rth; intros; constructor;  eauto.
-intros.
-apply reqb_ok.
-destruct (reqb x y); trivial; intros.
-elim H.
-Qed.
-
- Definition default_eqb : R -> R -> bool := fun x y => false.
- Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
-Proof.
-discriminate 1.
-Qed.
-
-End New2OldRing.
-
-Section New2OldSemiRing.
- Variable R : Type.
- Variable (rO rI : R) (radd rmul: R->R->R).
- Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
-
- Variable reqb : R -> R -> bool.
- Variable reqb_ok : forall x y, reqb x y = true -> x = y.
-
- Lemma sring_equiv2 :
-   Semi_Ring_Theory radd rmul rI rO reqb.
-Proof.
-elim SRth; intros; constructor;  eauto.
-intros.
-apply reqb_ok.
-destruct (reqb x y); trivial; intros.
-elim H.
-Qed.
-
-End New2OldSemiRing.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 21d3099c..2d2756b1 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1,17 +1,19 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+
 Set Implicit Arguments.
-Require Import Setoid Morphisms BinList BinPos BinNat BinInt.
+Require Import Setoid Morphisms. 
+Require Import BinList BinPos BinNat BinInt.
 Require Export Ring_theory.
-
 Local Open Scope positive_scope.
 Import RingSyntax.
+(* Set Universe Polymorphism. *)
 
 Section MakeRingPol.
 
@@ -372,17 +374,6 @@ Section MakeRingPol.
 
  Infix "**" := Pmul.
 
- Fixpoint Psquare (P:Pol) : Pol :=
-   match P with
-   | Pc c => Pc (c *! c)
-   | Pinj j Q => Pinj j (Psquare Q)
-   | PX P i Q =>
-     let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in
-     let Q2 := Psquare Q in
-     let P2 := Psquare P in
-     mkPX (mkPX P2 i P0 ++ twoPQ) i Q2
-   end.
-
  (** Monomial **)
 
  (** A monomial is X1^k1...Xi^ki. Its representation
@@ -511,6 +502,29 @@ Section MakeRingPol.
  Reserved Notation "P @ l " (at level 10, no associativity).
  Notation "P @ l " := (Pphi l P).
 
+ Definition Pequiv (P Q : Pol) := forall l, P@l == Q@l.
+ Infix "===" := Pequiv (at level 70, no associativity).
+
+ Instance Pequiv_eq : Equivalence Pequiv.
+ Proof.
+  unfold Pequiv; split; red; intros; [reflexivity|now symmetry|now etransitivity].
+ Qed.
+
+ Instance Pphi_ext : Proper (eq ==> Pequiv ==> req) Pphi.
+ Proof.
+  now intros l l' <- P Q H.
+ Qed.
+
+ Instance Pinj_ext : Proper (eq ==> Pequiv ==> Pequiv) Pinj.
+ Proof.
+  intros i j <- P P' HP l. simpl. now rewrite HP.
+ Qed.
+
+ Instance PX_ext : Proper (Pequiv ==> eq ==> Pequiv ==> Pequiv) PX.
+ Proof.
+  intros P P' HP p p' <- Q Q' HQ l. simpl. now rewrite HP, HQ.
+ Qed.
+
  (** Evaluation of a monomial towards R *)
 
  Fixpoint Mphi(l:list R) (M: Mon) : R :=
@@ -532,8 +546,9 @@ Section MakeRingPol.
  Lemma jump_add' i j (l:list R) : jump (i + j) l = jump j (jump i l).
  Proof. rewrite Pos.add_comm. apply jump_add. Qed.
 
- Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l.
+ Lemma Peq_ok P P' : (P ?== P') = true -> P === P'.
  Proof.
+  unfold Pequiv.
   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 ].
@@ -545,8 +560,7 @@ Section MakeRingPol.
     now rewrite IHP1, IHP2.
  Qed.
 
- Lemma Peq_spec P P' :
-   BoolSpec (forall l, P@l == P'@l) True (P ?== P').
+ Lemma Peq_spec P P' : BoolSpec (P === P') True (P ?== P').
  Proof.
   generalize (Peq_ok P P'). destruct (P ?== P'); auto.
  Qed.
@@ -567,6 +581,11 @@ Section MakeRingPol.
   now rewrite jump_add'.
  Qed.
 
+ Instance mkPinj_ext : Proper (eq ==> Pequiv ==> Pequiv) mkPinj.
+ Proof.
+  intros i j <- P Q H l. now rewrite !mkPinj_ok.
+ Qed.
+
  Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
  Proof.
   rewrite Pos.add_comm.
@@ -590,6 +609,11 @@ Section MakeRingPol.
     rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl.
  Qed.
 
+ Instance mkPX_ext : Proper (Pequiv ==> eq ==> Pequiv ==> Pequiv) mkPX.
+ Proof.
+  intros P P' HP i i' <- Q Q' HQ l. now rewrite !mkPX_ok, HP, HQ.
+ Qed.
+
  Hint Rewrite
   Pphi0
   Pphi1
@@ -656,7 +680,7 @@ Section MakeRingPol.
   - add_permut.
   - destruct p; simpl;
     rewrite ?jump_pred_double; add_permut.
-  - destr_pos_sub; intros ->;Esimpl.
+  - 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.
@@ -689,47 +713,23 @@ Section MakeRingPol.
         rewrite IHP'2, pow_pos_add; rsimpl. add_permut.
  Qed.
 
- 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.
+ Lemma Psub_opp P' P : P -- P' === P ++ (--P').
  Proof.
-  intros IHP'.
-  revert k l. induction P;simpl;intros.
-  - rewrite Popp_ok;rsimpl; add_permut.
-  - destruct p; simpl;
-    rewrite Popp_ok;rsimpl;
-    rewrite ?jump_pred_double; add_permut.
-  - destr_pos_sub; intros ->; Esimpl.
-    + rewrite IHP';rsimpl. add_permut.
-    + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut.
-    + rewrite IHP1, pow_pos_add;rsimpl. add_permut.
+  revert P; induction P'; simpl; intros.
+  - intro l; Esimpl.
+  - revert p; induction P; simpl; intros; try reflexivity.
+    + destr_pos_sub; intros ->; now apply mkPinj_ext.
+    + destruct p0; now apply PX_ext.
+  - destruct P; simpl; try reflexivity.
+    + destruct p0; now apply PX_ext.
+    + destr_pos_sub; intros ->; apply mkPX_ext; auto.
+      revert p1. induction P2; simpl; intros; try reflexivity.
+      destr_pos_sub; intros ->; now apply mkPX_ext.
  Qed.
 
  Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l.
  Proof.
-  revert P l; induction P';simpl;intros;Esimpl.
-  - revert p l; induction P;simpl;intros.
-    + Esimpl; add_permut.
-    + destr_pos_sub; intros ->;Esimpl.
-      * rewrite IHP';rsimpl.
-      * rewrite IHP';Esimpl. now rewrite jump_add'.
-      * rewrite IHP. now rewrite jump_add'.
-    + destruct p0;simpl.
-      * rewrite IHP2;simpl. rsimpl.
-      * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl.
-      * rewrite IHP'. rsimpl.
-  - destruct P;simpl.
-    + Esimpl; add_permut.
-    + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl.
-      * rsimpl. add_permut.
-      * rewrite jump_pred_double. rsimpl. add_permut.
-      * rsimpl. add_permut.
-    + destr_pos_sub; intros ->; Esimpl.
-      * rewrite IHP'1, IHP'2;rsimpl. add_permut.
-      * rewrite IHP'1, IHP'2;simpl;Esimpl.
-        rewrite pow_pos_add;rsimpl. add_permut.
-      * rewrite PsubX_ok by trivial;rsimpl.
-        rewrite IHP'2, pow_pos_add;rsimpl. add_permut.
+  rewrite Psub_opp, Padd_ok, Popp_ok. rsimpl.
  Qed.
 
  Lemma PmulI_ok P' :
@@ -764,15 +764,6 @@ Section MakeRingPol.
       add_permut; f_equiv; mul_permut.
  Qed.
 
- Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l.
- Proof.
-  revert l;induction P;simpl;intros;Esimpl.
-  - apply IHP.
-  - rewrite Padd_ok, Pmul_ok;Esimpl.
-    rewrite IHP1, IHP2.
-    mul_push ((hd l)^p). now mul_push (P2@l).
- Qed.
-
  Lemma mkZmon_ok M j l :
    (mkZmon j M) @@ l == (zmon j M) @@ l.
  Proof.
@@ -807,9 +798,9 @@ Section MakeRingPol.
      P@l == Q@l + [c] * R@l.
  Proof.
  revert l.
- induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl.
- - assert (H := div_th.(div_eucl_th) c0 c).
-   destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
+ induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. 
+ - assert (H := div_th.(div_eucl_th) c0 c). 
+   destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. 
  - destr_factor. Esimpl.
  - destr_factor. Esimpl. add_permut.
  Qed.
@@ -818,11 +809,12 @@ Section MakeRingPol.
    let (c,M) := cM in
    let (Q,R) := MFactor P c M in
      P@l == Q@l + [c] * M@@l * R@l.
- Proof.
+ Proof. 
  destruct cM as (c,M). revert M l.
- induction P; destruct M; intros l; simpl; auto;
+ induction P; destruct M; intros l; simpl; auto; 
  try (case ceqb_spec; intro He);
-  try (case Pos.compare_spec; intros He); rewrite ?He;
+  try (case Pos.compare_spec; intros He);
+  rewrite ?He;
    destr_factor; simpl; Esimpl.
  - assert (H := div_th.(div_eucl_th) c0 c).
    destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
@@ -880,9 +872,9 @@ Section MakeRingPol.
  Lemma PSubstL1_ok n LM1 P1 l :
    MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l.
  Proof.
- revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros.
- - reflexivity.
- - rewrite <- IH by intuition. now apply PNSubst1_ok.
+ revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. 
+ - reflexivity. 
+ - rewrite <- IH by intuition; now apply PNSubst1_ok.
  Qed.
 
  Lemma PSubstL_ok n LM1 P1 P2 l :
@@ -907,6 +899,8 @@ Section MakeRingPol.
  (** Definition of polynomial expressions *)
 
  Inductive PExpr : Type :=
+  | PEO : PExpr
+  | PEI : PExpr            
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
   | PEadd : PExpr -> PExpr -> PExpr
@@ -915,6 +909,7 @@ Section MakeRingPol.
   | PEopp : PExpr -> PExpr
   | PEpow : PExpr -> N -> PExpr.
 
+
  (** evaluation of polynomial expressions towards R *)
  Definition mk_X j := mkPinj_pred j mkX.
 
@@ -922,6 +917,8 @@ Section MakeRingPol.
 
  Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
    match pe with
+   | PEO => rO
+   | PEI => rI
    | PEc c => phi c
    | PEX j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
@@ -985,11 +982,13 @@ Section POWER.
   Variable n : nat.
   Variable lmp:list (C*Mon*Pol).
   Let subst_l P := PNSubstL P lmp n n.
-  Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
+  Let Pmul_subst P1 P2 := subst_l (P1 ** P2).
   Let Ppow_subst := Ppow_N subst_l.
 
   Fixpoint norm_aux (pe:PExpr) : Pol :=
    match pe with
+   | PEO => Pc cO
+   | PEI => Pc cI
    | PEc c => Pc c
    | PEX j => mk_X j
    | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1)
@@ -1021,7 +1020,7 @@ Section POWER.
     end.
   Proof.
   simpl (norm_aux (PEadd _ _)).
-  destruct pe1; [ | | | | | reflexivity | ];
+  destruct pe1; [ | | | | | | | reflexivity | ];
    destruct pe2; simpl get_PEopp; reflexivity.
   Qed.
 
@@ -1034,22 +1033,26 @@ Section POWER.
   now destruct pe.
   Qed.
 
+  Arguments norm_aux !pe : simpl nomatch.
+
   Lemma norm_aux_spec l pe :
     PEeval l pe == (norm_aux pe)@l.
   Proof.
    intros.
-   induction pe.
+   induction pe; cbn.
+   - now rewrite (morph0 CRmorph). 
+   - now rewrite (morph1 CRmorph).
    - reflexivity.
    - apply mkX_ok.
-   - simpl PEeval. rewrite IHpe1, IHpe2.
+   - 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 IHpe1, IHpe2. Esimpl.
+   - rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
+   - rewrite IHpe. Esimpl.
+   - 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.
@@ -1483,3 +1486,6 @@ Qed.
  Qed.
 
 End MakeRingPol.
+
+Arguments PEO [C].
+Arguments PEI [C].
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 7a7ffcfd..77863edc 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -196,12 +196,17 @@ Ltac get_MonPol lemma :=
 (********************************************************)
 
 (* Building the atom list of a ring expression *)
-Ltac FV Cst CstPow add mul sub opp pow t fv :=
+(* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+(* the tactic could be used to discriminate occurrences of an opaque *)
+(* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac FV Cst CstPow rO rI add mul sub opp pow t fv :=
  let rec TFV t fv :=
   let f :=
   match Cst t with
   | NotConstant =>
       match t with
+      | rO =>  fun _ => fv
+      | rI =>  fun _ => fv
       | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
       | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
@@ -219,32 +224,39 @@ Ltac FV Cst CstPow add mul sub opp pow t fv :=
  in TFV t fv.
 
  (* syntaxification of ring expressions *)
-Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv :=
  let rec mkP t :=
     let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with
+        | rO => 
+          fun _ => constr:(@PEO C)
+        | rI => 
+          fun _ => constr:(@PEI C)
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEadd e1 e2)
+          let e2 := mkP t2 in constr:(@PEadd C e1 e2)
         | (rmul ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEmul e1 e2)
+          let e2 := mkP t2 in constr:(@PEmul C e1 e2)
         | (rsub ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(PEsub e1 e2)
+          let e2 := mkP t2 in constr:(@PEsub C e1 e2)
         | (ropp ?t1) =>
           fun _ =>
-          let e1 := mkP t1 in constr:(PEopp e1)
+          let e1 := mkP t1 in constr:(@PEopp C e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant =>
             fun _ => let p := Find_at t fv in constr:(PEX C p)
-          | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(@PEpow C e1 c)
           end
         | _ =>
           fun _ => let p := Find_at t fv in constr:(PEX C p)
@@ -260,58 +272,58 @@ Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post :=
   let RNG :=
     match type of lemma1 with
     | context
-       [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+       [@PEeval ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
         (fun proj => proj
              cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2)
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2)
     | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
     end in
   F RNG.
 
 Ltac get_Carrier RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             R).
 
 Ltac get_Eq RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             req).
 
 Ltac get_Pre RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             pre).
 
 Ltac get_Post RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             post).
 
 Ltac get_NormLemma RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             lemma1).
 
 Ltac get_SimplifyLemma RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             lemma2).
 
 Ltac get_RingFV RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-            FV cst_tac pow_tac add mul sub opp pow).
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            FV cst_tac pow_tac r0 r1 add mul sub opp pow).
 
 Ltac get_RingMeta RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-            mkPolexpr C cst_tac pow_tac add mul sub opp pow).
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow).
 
 Ltac get_RingHypTac RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-       let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+       let mkPol := mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow in
        fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
 
 (* ring tactics *)
@@ -338,8 +350,8 @@ Ltac Ring RNG lemma lH :=
     (apply (lemma vfv vlpe pe1 pe2)
       || fail "typing error while applying ring");
     [ ((let prh := proofHyp_tac lH in exact prh)
-        || idtac "can not automatically proof hypothesis :";
-           idtac " maybe a left member of a hypothesis is not a monomial")
+        || idtac "can not automatically prove hypothesis :";
+           [> idtac " maybe a left member of a hypothesis is not a monomial"..])
     | vm_compute;
       (exact (eq_refl true) || fail "not a valid ring equation")]).
 
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index af43b0ab..4f05f0d4 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -28,6 +28,8 @@ Reserved Notation "x == y" (at level 70, no associativity).
 End RingSyntax.
 Import RingSyntax.
 
+(* Set Universe Polymorphism. *)
+
 Section Power.
  Variable R:Type.
  Variable rI : R.
@@ -252,6 +254,7 @@ Section ALMOST_RING.
 
  Section SEMI_RING.
  Variable SReqe : sring_eq_ext radd rmul req.
+
    Add Morphism radd : radd_ext1.  exact (SRadd_ext SReqe). Qed.
    Add Morphism rmul : rmul_ext1.  exact (SRmul_ext SReqe). Qed.
  Variable SRth : semi_ring_theory 0 1 radd rmul req.
@@ -503,7 +506,6 @@ Qed.
 
 End ALMOST_RING.
 
-
 Section AddRing.
 
 (* Variable R : Type.
@@ -528,7 +530,6 @@ Inductive ring_kind : Type :=
     (_ : ring_morph rO rI radd rmul rsub ropp req
                     cO cI cadd cmul csub copp ceqb phi).
 
-
 End AddRing.
 
 
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index 58a4d7ea..605a23a9 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -1,6 +1,7 @@
 Require Export Cring.
 Require Export Integral_domain.
 Require Export Ncring_initial.
+Require Export Omega.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 1177688d..848e06a7 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -48,8 +48,8 @@ Ltac Zpower_neg :=
 Add Ring Zr : Zth
   (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ],
    power_tac Zpower_theory [Zpow_tac],
-    (* The two following option are not needed, it is the default chose when the set of
-        coefficiant is usual ring Z *)
+    (* The following two options are not needed; they are the default choice
+       when the set of coefficient is the usual ring Z *)
     div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)),
    sign get_signZ_th).
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index d1a5c0ab..2f9e8509 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -1,30 +1,27 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
+open Vars
 open Closure
 open Environ
 open Libnames
-open Tactics
+open Globnames
 open Glob_term
 open Tacticals
 open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
 open Coqlib
-open Tacmach
 open Mod_subst
 open Tacinterp
 open Libobject
@@ -32,14 +29,20 @@ open Printer
 open Declare
 open Decl_kinds
 open Entries
+open Misctypes
+
+DECLARE PLUGIN "newring_plugin"
 
 (****************************************************************************)
 (* controlled reduction *)
 
-let mark_arg i c = mkEvar(i,[|c|])
+(** ppedrot: something dubious here, we're obviously using evars the wrong
+    way. FIXME! *)
+
+let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|])
 let unmark_arg f c =
   match destEvar c with
-    | (i,[|c|]) -> f i c
+    | (i,[|c|]) -> f (Evar.repr i) c
     | _ -> assert false
 
 type protect_flag = Eval|Prot|Rec
@@ -48,10 +51,19 @@ let tag_arg tag_rec map subs i c =
   match map i with
       Eval -> mk_clos subs c
     | Prot -> mk_atom c
-    | Rec -> if i = -1 then mk_clos subs c else tag_rec c
+    | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
+
+let global_head_of_constr c = 
+  let f, args = decompose_app c in
+    try global_of_constr f
+    with Not_found -> anomaly (str "global_head_of_constr")
+
+let global_of_constr_nofail c = 
+  try global_of_constr c
+  with Not_found -> VarRef (Id.of_string "dummy")
 
 let rec mk_clos_but f_map subs t =
-  match f_map t with
+  match f_map (global_of_constr_nofail t) with
     | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
     | None ->
         (match kind_of_term t with
@@ -62,9 +74,9 @@ let rec mk_clos_but f_map subs t =
 and mk_clos_app_but f_map subs f args n =
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
-    let fargs, args' = array_chop n args in
+    let fargs, args' = Array.chop n args in
     let f' = mkApp(f,fargs) in
-    match f_map f' with
+    match f_map (global_of_constr_nofail f') with
         Some map ->
           mk_clos_deep
             (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
@@ -72,24 +84,13 @@ and mk_clos_app_but f_map subs f args n =
             (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
       | None -> mk_clos_app_but f_map subs f args (n+1)
 
-
-let interp_map l c =
-  try
-    let (im,am) = List.assoc c l in
-    Some(fun i ->
-      if List.mem i im then Eval
-      else if List.mem i am then Prot
-      else if i = -1 then Eval
-      else Rec)
-  with Not_found -> None
-
 let interp_map l t =
-  try Some(list_assoc_f eq_constr t l) with Not_found -> None
+  try Some(List.assoc_f eq_gr t l) with Not_found -> None
 
-let protect_maps = ref Stringmap.empty
-let add_map s m = protect_maps := Stringmap.add s m !protect_maps
+let protect_maps = ref String.Map.empty
+let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
-  try Stringmap.find map !protect_maps
+  try String.Map.find map !protect_maps
   with Not_found ->
     errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
 
@@ -101,112 +102,120 @@ let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));;
+  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));;
 
 
 TACTIC EXTEND protect_fv
   [ "protect_fv" string(map) "in" ident(id) ] ->
-    [ protect_tac_in map id ]
+    [ Proofview.V82.tactic (protect_tac_in map id) ]
 | [ "protect_fv" string(map) ] ->
-    [ protect_tac map ]
+    [ Proofview.V82.tactic (protect_tac map) ]
 END;;
 
 (****************************************************************************)
 
 let closed_term t l =
-  let l = List.map constr_of_global l in
+  let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
 ;;
 
 TACTIC EXTEND closed_term
   [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term t l ]
+    [ Proofview.V82.tactic (closed_term t l) ]
 END
 ;;
 
-TACTIC EXTEND echo
+(* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
   [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
-END;;
+END;;*)
 
 (*
 let closed_term_ast l =
-  TacFun([Some(id_of_string"t")],
-  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
-  [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t"));
-   Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l])))
+  TacFun([Some(Id.of_string"t")],
+  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
+  [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
+   Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
 *)
 let closed_term_ast l =
-  let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in
-  TacFun([Some(id_of_string"t")],
-  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
-  [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None);
-   Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
+  let tacname = {
+    mltac_plugin = "newring_plugin";
+    mltac_tactic = "closed_term";
+  } in
+  let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
+  TacFun([Some(Id.of_string"t")],
+  TacML(Loc.ghost,tacname,
+  [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
+   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l]))
 (*
-let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
+let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
 
 (****************************************************************************)
 
 let ic c =
   let env = Global.env() and sigma = Evd.empty in
-  Constrintern.interp_constr sigma env c
+  Constrintern.interp_open_constr env sigma c
+
+let ic_unsafe c = (*FIXME remove *)
+  let env = Global.env() and sigma = Evd.empty in
+    fst (Constrintern.interp_constr env sigma c)
 
 let ty c = Typing.type_of (Global.env()) Evd.empty c
 
-let decl_constant na c =
-  mkConst(declare_constant (id_of_string na) (DefinitionEntry
-    { const_entry_body = c;
-      const_entry_secctx = None;
-      const_entry_type = None;
-      const_entry_opaque = true },
-    IsProof Lemma))
+let decl_constant na ctx c =
+  let vars = Universes.universes_of_constr c in
+  let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
+  mkConst(declare_constant (Id.of_string na) 
+	    (DefinitionEntry (definition_entry ~opaque:true
+				~univs:(Univ.ContextSet.to_context ctx) c),
+	     IsProof Lemma))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
 
 let ltac_letin (x, e1) e2 =
-  TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
+  TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2)
 
 let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) =
   Tacinterp.eval_tactic
     (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args))
 
 let ltac_record flds =
-  TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds)
+  TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
 
 
-let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
+let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
 
-let dummy_goal env =
+let dummy_goal env sigma =
   let (gl,_,sigma) = 
-    Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
-  {Evd.it = gl;
-   Evd.sigma = sigma}
+    Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in
+  {Evd.it = gl; Evd.sigma = sigma}
 
-let exec_tactic env n f args =
-  let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
+let constr_of v = match Value.to_constr v with
+  | Some c -> c
+  | None -> failwith "Ring.exec_tactic: anomaly"
+
+let exec_tactic env evd n f args =
+  let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let res = ref [||] in
   let get_res ist =
-    let l = List.map (fun id ->  List.assoc id ist.lfun) lid in
+    let l = List.map (fun id ->  Id.Map.find id ist.lfun) lid in
     res := Array.of_list l;
     TacId[] in
   let getter =
     Tacexp(TacFun(List.map(fun id -> Some id) lid,
-                  glob_tactic(tacticIn get_res))) in
-  let _ =
-    Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
-  !res
-
-let constr_of = function
-  | VConstr ([],c) -> c
-  | _ -> failwith "Ring.exec_tactic: anomaly"
+                  Tacintern.glob_tactic(tacticIn get_res))) in
+  let gl = dummy_goal env evd in
+  let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) gl in
+  let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
+    Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
@@ -217,16 +226,23 @@ let stdlib_modules =
 
 let coq_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
+let coq_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
 let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
-let coq_cons = coq_constant "cons"
-let coq_nil = coq_constant "nil"
-let coq_None = coq_constant "None"
-let coq_Some = coq_constant "Some"
+let coq_None = coq_reference "None"
+let coq_Some = coq_reference "Some"
 let coq_eq = coq_constant "eq"
 
+let coq_cons = coq_reference "cons"
+let coq_nil = coq_reference "nil"
+
 let lapp f args = mkApp(Lazy.force f,args)
 
+let plapp evd f args = 
+  let fc = Evarutil.e_new_global evd (Lazy.force f) in
+    mkApp(fc,args)
+
 let dest_rel0 t =
   match kind_of_term t with
   | App(f,args) when Array.length args >= 2 ->
@@ -255,17 +271,19 @@ let plugin_modules =
 
 let my_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
+let my_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
-  make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"])
+  DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s))
 let znew_ring_path =
-  make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"])
+  DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
 
-let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
+let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 
 (* Ring theory *)
@@ -274,9 +292,9 @@ let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 let coq_almost_ring_theory = my_constant "almost_ring_theory"
 
 (* setoid and morphism utilities *)
-let coq_eq_setoid = my_constant "Eqsth"
-let coq_eq_morph = my_constant "Eq_ext"
-let coq_eq_smorph = my_constant "Eq_s_ext"
+let coq_eq_setoid = my_reference "Eqsth"
+let coq_eq_morph = my_reference "Eq_ext"
+let coq_eq_smorph = my_reference "Eq_s_ext"
 
 (* ring -> almost_ring utilities *)
 let coq_ring_theory = my_constant "ring_theory"
@@ -303,16 +321,19 @@ let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
 let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
 
 (* hypothesis *)
-let coq_mkhypo = my_constant "mkhypo"
-let coq_hypo = my_constant "hypo"
+let coq_mkhypo = my_reference "mkhypo"
+let coq_hypo = my_reference "hypo"
 
 (* Equality: do not evaluate but make recursive call on both sides *)
 let map_with_eq arg_map c =
   let (req,_,_) = dest_rel c in
   interp_map
-    ((req,(function -1->Prot|_->Rec))::
+    ((global_head_of_constr req,(function -1->Prot|_->Rec))::
     List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
 
+let map_without_eq arg_map _ =
+  interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
+
 let _ = add_map "ring"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
@@ -343,15 +364,12 @@ type ring_info =
       ring_pre_tac : glob_tactic_expr;
       ring_post_tac : glob_tactic_expr }
 
-module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
+module Cmap = Map.Make(Constr)
 
-let from_carrier = ref Cmap.empty
-let from_relation = ref Cmap.empty
-let from_name = ref Spmap.empty
+let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
+let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
 
 let ring_for_carrier r = Cmap.find r !from_carrier
-let ring_for_relation rel = Cmap.find rel !from_relation
-
 
 let find_ring_structure env sigma l =
   match l with
@@ -370,32 +388,9 @@ let find_ring_structure env sigma l =
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
-(*
-        let (req,_,_) = dest_rel cl in
-        (try ring_for_relation req
-        with Not_found ->
-          errorlabstrm "ring"
-            (str"cannot find a declared ring structure for equality"++
-             spc()++str"\""++pr_constr req++str"\"")) *)
-
-let _ =
-  Summary.declare_summary "tactic-new-ring-table"
-    { Summary.freeze_function =
-        (fun () -> !from_carrier,!from_relation,!from_name);
-      Summary.unfreeze_function =
-        (fun (ct,rt,nt) ->
-          from_carrier := ct; from_relation := rt; from_name := nt);
-      Summary.init_function =
-        (fun () ->
-          from_carrier := Cmap.empty; from_relation := Cmap.empty;
-          from_name := Spmap.empty) }
 
 let add_entry (sp,_kn) e =
-(*  let _ = ty e.ring_lemma1 in
-  let _ = ty e.ring_lemma2 in
-*)
   from_carrier := Cmap.add e.ring_carrier e !from_carrier;
-  from_relation := Cmap.add e.ring_req e !from_relation;
   from_name := Spmap.add sp e !from_name
 
 
@@ -408,10 +403,10 @@ let subst_th (subst,th) =
   let th' = subst_mps subst th.ring_th in
   let thm1' = subst_mps subst th.ring_lemma1 in
   let thm2' = subst_mps subst th.ring_lemma2 in
-  let tac'= subst_tactic subst th.ring_cst_tac in
-  let pow_tac'= subst_tactic subst th.ring_pow_tac in
-  let pretac'= subst_tactic subst th.ring_pre_tac in
-  let posttac'= subst_tactic subst th.ring_post_tac in
+  let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in
+  let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
      eq_constr set' th.ring_setoid &&
@@ -443,20 +438,20 @@ let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
-      open_function = (fun i o -> if i=1 then cache_th o);
+      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x)}
 
 
-let setoid_of_relation env a r =
-  let evm = Evd.empty in
+let setoid_of_relation env evd a r =
   try
-    lapp coq_mk_Setoid
-      [|a ; r ;
-	Rewrite.get_reflexive_proof env evm a r ;
-	Rewrite.get_symmetric_proof env evm a r ;
-	Rewrite.get_transitive_proof env evm a r |]
+    let evm = !evd in
+    let evm, refl = Rewrite.get_reflexive_proof env evm a r in
+    let evm, sym = Rewrite.get_symmetric_proof env evm a r in
+    let evm, trans = Rewrite.get_transitive_proof env evm a r in
+      evd := evm;
+      lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
     error "cannot find setoid relation"
 
@@ -469,7 +464,7 @@ let op_smorph r add mul req m1 m2 =
 (* let default_ring_equality (r,add,mul,opp,req) = *)
 (*   let is_setoid = function *)
 (*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(*         eq_constr req rel (\* Qu: use conversion ? *\) *)
+(*         eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
 (*     | _ -> false in *)
 (*   match default_relation_for_carrier ~filter:is_setoid r with *)
 (*       Leibniz _ -> *)
@@ -484,7 +479,7 @@ let op_smorph r add mul req m1 m2 =
 (*         let is_endomorphism = function *)
 (*             { args=args } -> List.for_all *)
 (*                 (function (var,Relation rel) -> *)
-(*                   var=None && eq_constr req rel *)
+(*                   var=None && eq_constr_nounivs req rel *)
 (*                   | _ -> false) args in *)
 (*         let add_m = *)
 (*           try default_morphism ~filter:is_endomorphism add *)
@@ -519,17 +514,19 @@ let op_smorph r add mul req m1 m2 =
 (*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
 (*         (setoid,op_morph) *)
 
-let ring_equality (r,add,mul,opp,req) =
+let ring_equality env evd (r,add,mul,opp,req) =
   match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
-	let setoid = lapp coq_eq_setoid [|r|] in
+    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
+	let setoid = plapp evd coq_eq_setoid [|r|] in
 	let op_morph =
 	  match opp with
-              Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
-            | None -> lapp coq_eq_smorph [|r;add;mul|] in
+              Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
+            | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+	let setoid = Typing.solve_evars env evd setoid in
+	let op_morph = Typing.solve_evars env evd op_morph in
 	  (setoid,op_morph)
     | _ ->
-	let setoid = setoid_of_relation (Global.env ()) r req in
+	let setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
 	let add_m, add_m_lem =
 	  try Rewrite.default_morphism signature add
@@ -549,7 +546,7 @@ let ring_equality (r,add,mul,opp,req) =
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
-		    msgnl
+		    msg_info
 		    (str"Using setoid \""++pr_constr req++str"\""++spc()++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
@@ -558,7 +555,7 @@ let ring_equality (r,add,mul,opp,req) =
 		  op_morph)
             | None ->
 		(Flags.if_verbose
-		    msgnl
+		    msg_info
 		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\""++spc()++str"and \""++
@@ -566,22 +563,22 @@ let ring_equality (r,add,mul,opp,req) =
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
-let build_setoid_params r add mul opp req eqth =
+let build_setoid_params env evd r add mul opp req eqth =
   match eqth with
       Some th -> th
-    | None -> ring_equality (r,add,mul,opp,req)
+    | None -> ring_equality env evd (r,add,mul,opp,req)
 
 let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
   match kind_of_term th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr f (Lazy.force coq_almost_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) ->
           (None,r,zero,one,add,mul,Some sub,Some opp,req)
     | App(f,[|r;zero;one;add;mul;req|])
-        when eq_constr f (Lazy.force coq_semi_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) ->
         (Some true,r,zero,one,add,mul,None,None,req)
     | App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr f (Lazy.force coq_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_ring_theory) ->
         (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"
 
@@ -591,18 +588,18 @@ let dest_morph env sigma m_spec =
   match kind_of_term m_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req;
               c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when eq_constr f (Lazy.force coq_ring_morph) ->
+        when eq_constr_nounivs f (Lazy.force coq_ring_morph) ->
           (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
     | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when eq_constr f (Lazy.force coq_semi_morph) ->
+        when eq_constr_nounivs f (Lazy.force coq_semi_morph) ->
         (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
     | _ -> error "bad morphism structure"
 
 
-type coeff_spec =
-    Computational of constr (* equality test *)
+type 'constr coeff_spec =
+    Computational of 'constr (* equality test *)
   | Abstract (* coeffs = Z *)
-  | Morphism of constr (* general morphism *)
+  | Morphism of 'constr (* general morphism *)
 
 
 let reflect_coeff rkind =
@@ -618,101 +615,89 @@ type cst_tac_spec =
 
 let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
-      Some (CstTac t) -> Tacinterp.glob_tactic t
+      Some (CstTac t) -> Tacintern.glob_tactic t
     | Some (Closed lc) ->
         closed_term_ast (List.map Smartlocate.global_with_alias lc)
     | None ->
-        (match rk, opp, kind with
-            Abstract, None, _ ->
-              let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
-              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
-          | Abstract, Some opp, Some _ ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
-              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | Abstract, Some opp, None ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
-              TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | Computational _,_,_ ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
-              TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
-          | Morphism mth,_,_ ->
-              let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
-              TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
-
-let make_hyp env c =
-  let t = Retyping.get_type_of env Evd.empty c in
-  lapp coq_mkhypo [|t;c|]
-
-let make_hyp_list env lH =
-  let carrier = Lazy.force coq_hypo in
-  List.fold_right
-    (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH
-    (lapp coq_nil [|carrier|])
-
-let interp_power env pow =
-  let carrier = Lazy.force coq_hypo in
+        let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
+              TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
+
+let make_hyp env evd c =
+  let t = Retyping.get_type_of env !evd c in
+   plapp evd coq_mkhypo [|t;c|]
+
+let make_hyp_list env evd lH =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+  let l = 
+    List.fold_right
+      (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
+      (plapp evd coq_nil [|carrier|])
+  in 
+  let l' = Typing.solve_evars env evd l in
+    Evarutil.nf_evars_universes !evd l'
+
+let interp_power env evd pow =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match pow with
   | None ->
-      let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+      let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
+      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
-        | CstTac t -> Tacinterp.glob_tactic t
+        | CstTac t -> Tacintern.glob_tactic t
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
-      let spec = make_hyp env (ic spec) in
-      (tac, lapp coq_Some [|carrier; spec|])
+      let spec = make_hyp env evd (ic_unsafe spec) in
+      (tac, plapp evd coq_Some [|carrier; spec|])
 
-let interp_sign env sign =
-  let carrier = Lazy.force coq_hypo in
+let interp_sign env evd sign =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match sign with
-  | None -> lapp coq_None [|carrier|]
+  | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env (ic spec) in
-      lapp coq_Some [|carrier;spec|]
+      let spec = make_hyp env evd (ic_unsafe spec) in
+      plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let interp_div env div =
-  let carrier = Lazy.force coq_hypo in
+let interp_div env evd div =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match div with
-  | None -> lapp coq_None [|carrier|]
+  | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env (ic spec) in
-      lapp coq_Some [|carrier;spec|]
+      let spec = make_hyp env evd (ic_unsafe spec) in
+      plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
+let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
   check_required_library (cdir@["Ring_base"]);
   let env = Global.env() in
-  let sigma = Evd.empty in
   let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
-  let (sth,ext) = build_setoid_params r add mul opp req eqth in
-  let (pow_tac, pspec) = interp_power env power in
-  let sspec = interp_sign env sign in
-  let dspec = interp_div env div in
+  let evd = ref sigma in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
+  let (pow_tac, pspec) = interp_power env evd power in
+  let sspec = interp_sign env evd sign in
+  let dspec = interp_div env evd div in
   let rk = reflect_coeff morphth in
-  let params =
-    exec_tactic env 5 (zltac "ring_lemmas")
+  let params,ctx =
+    exec_tactic env !evd 5 (zltac "ring_lemmas")
       (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in
-  let lemma1 = constr_of params.(3) in
-  let lemma2 = constr_of params.(4) in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
 
-  let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
-  let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
+  let lemma1 =
+    decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in
+  let lemma2 =
+    decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let posttac =
     match post with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
@@ -720,9 +705,9 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
         { ring_carrier = r;
           ring_req = req;
           ring_setoid = sth;
-          ring_ext = constr_of params.(1);
-          ring_morph = constr_of params.(2);
-          ring_th = constr_of params.(0);
+          ring_ext = params.(1);
+          ring_morph = params.(2);
+          ring_th = params.(0);
           ring_cst_tac = cst_tac;
 	  ring_pow_tac = pow_tac;
           ring_lemma1 = lemma1;
@@ -731,22 +716,28 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
           ring_post_tac = posttac }) in
   ()
 
-type ring_mod =
-    Ring_kind of coeff_spec
+type 'constr ring_mod =
+    Ring_kind of 'constr coeff_spec
   | Const_tac of cst_tac_spec
   | Pre_tac of raw_tactic_expr
   | Post_tac of raw_tactic_expr
-  | Setoid of Topconstr.constr_expr * Topconstr.constr_expr
-  | Pow_spec of cst_tac_spec * Topconstr.constr_expr
+  | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr
+  | Pow_spec of cst_tac_spec * Constrexpr.constr_expr
            (* Syntaxification tactic , correctness lemma *)
-  | Sign_spec of Topconstr.constr_expr
-  | Div_spec of Topconstr.constr_expr
+  | Sign_spec of Constrexpr.constr_expr
+  | Div_spec of Constrexpr.constr_expr
+
+
+let ic_coeff_spec = function
+  | Computational t -> Computational (ic_unsafe t)
+  | Morphism t -> Morphism (ic_unsafe t)
+  | Abstract -> Abstract
 
 
 VERNAC ARGUMENT EXTEND ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ]
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
   | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic morph)) ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
   | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
   | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
   | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
@@ -761,7 +752,7 @@ VERNAC ARGUMENT EXTEND ring_mod
 END
 
 let set_once s r v =
-  if !r = None then r := Some v else error (s^" cannot be set twice")
+  if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
 
 let process_ring_mods l =
   let kind = ref None in
@@ -773,21 +764,29 @@ let process_ring_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_kind k -> set_once "ring kind" kind k
+      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
     | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
     | Pre_tac t -> set_once "preprocess tactic" pre t
     | Post_tac t -> set_once "postprocess tactic" post t
-    | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)
+    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
     | Pow_spec(t,spec) -> set_once "power" power (t,spec)
     | Sign_spec t -> set_once "sign" sign t
     | Div_spec t -> set_once "div" div t) l;
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidRing
+VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
     [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
       add_theory id (ic t) set k cst (pre,post) power sign div]
+  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
+    msg_notice (strbrk "The following ring structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.ring_req))
+    ) !from_name ]
 END
 
 (*****************************************************************************)
@@ -799,10 +798,11 @@ let make_args_list rl t =
   | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2]
   | _ -> rl
 
-let make_term_list carrier rl =
-  List.fold_right
-    (fun x l -> lapp coq_cons [|carrier;x;l|]) rl
-    (lapp coq_nil [|carrier|])
+let make_term_list env evd carrier rl =
+  let l = List.fold_right
+    (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
+    (plapp evd coq_nil [|carrier|])
+  in Typing.solve_evars env evd l
 
 let ltac_ring_structure e =
   let req = carg e.ring_req in
@@ -819,19 +819,24 @@ let ltac_ring_structure e =
   [req;sth;ext;morph;th;cst_tac;pow_tac;
    lemma1;lemma2;pretac;posttac]
 
-let ring_lookup (f:glob_tactic_expr) lH rl t gl =
-  let env = pf_env gl in
-  let sigma = project gl in
-  let rl = make_args_list rl t in
-  let e = find_ring_structure env sigma rl in
-  let rl = carg (make_term_list e.ring_carrier rl) in
-  let lH = carg (make_hyp_list env lH) in
-  let ring = ltac_ring_structure e in
-  ltac_apply f (ring@[lH;rl]) gl
+let ring_lookup (f:glob_tactic_expr) lH rl t =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try (* find_ring_strucure can raise an exception *)
+      let evdref = ref sigma in
+      let rl = make_args_list rl t in
+      let e = find_ring_structure env sigma rl in
+      let rl = carg (make_term_list env evdref e.ring_carrier rl) in
+      let lH = carg (make_hyp_list env evdref lH) in
+      let ring = ltac_ring_structure e in
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t]
+    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t]
 END
 
 
@@ -839,10 +844,10 @@ END
 (***********************************************************************)
 
 let new_field_path =
-  make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"])
+  DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s))
 
 
 let _ = add_map "field"
@@ -851,9 +856,9 @@ let _ = add_map "field"
     coq_nil, (function -1->Eval|_ -> Prot);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
-    my_constant "display_linear",
+    my_reference "display_linear",
       (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
-    my_constant "display_pow_linear",
+    my_reference "display_pow_linear",
      (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
@@ -865,16 +870,16 @@ let _ = add_map "field"
     pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
     (* FEeval: evaluate morphism, protect field
        operations and make recursive call on the var map *)
-    my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
-  (map_with_eq
+  (map_without_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
      coq_nil, (function -1->Eval|_ -> Prot);
     (* PCond: evaluate morphism and denum list, protect ring
        operations and make recursive call on the var map *)
-     my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);;
-(*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
+     my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
+(*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
 
 
 let _ = Redexpr.declare_reduction "simpl_field_expr"
@@ -882,29 +887,29 @@ let _ = Redexpr.declare_reduction "simpl_field_expr"
 
 
 
-let afield_theory = my_constant "almost_field_theory"
-let field_theory = my_constant "field_theory"
-let sfield_theory = my_constant "semi_field_theory"
-let af_ar = my_constant"AF_AR"
-let f_r = my_constant"F_R"
-let sf_sr = my_constant"SF_SR"
-let dest_field env sigma th_spec =
-  let th_typ = Retyping.get_type_of env sigma th_spec in
+let afield_theory = my_reference "almost_field_theory"
+let field_theory = my_reference "field_theory"
+let sfield_theory = my_reference "semi_field_theory"
+let af_ar = my_reference"AF_AR"
+let f_r = my_reference"F_R"
+let sf_sr = my_reference"SF_SR"
+let dest_field env evd th_spec =
+  let th_typ = Retyping.get_type_of env !evd th_spec in
   match kind_of_term th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr f (Lazy.force afield_theory) ->
-        let rth = lapp af_ar
+        when is_global (Lazy.force afield_theory) f ->
+        let rth = plapp evd af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr f (Lazy.force field_theory) ->
+        when is_global (Lazy.force field_theory) f ->
         let rth =
-          lapp f_r
+          plapp evd f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when eq_constr f (Lazy.force sfield_theory) ->
-        let rth = lapp sf_sr
+        when is_global (Lazy.force sfield_theory) f ->
+        let rth = plapp evd sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
     | _ -> error "bad field structure"
@@ -922,13 +927,10 @@ type field_info =
       field_pre_tac : glob_tactic_expr;
       field_post_tac : glob_tactic_expr }
 
-let field_from_carrier = ref Cmap.empty
-let field_from_relation = ref Cmap.empty
-let field_from_name = ref Spmap.empty
-
+let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
+let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
 let field_for_carrier r = Cmap.find r !field_from_carrier
-let field_for_relation rel = Cmap.find rel !field_from_relation
 
 let find_field_structure env sigma l =
   check_required_library (cdir@["Field_tac"]);
@@ -948,35 +950,9 @@ let find_field_structure env sigma l =
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
-(*        let (req,_,_) = dest_rel cl in
-        (try field_for_relation req
-        with Not_found ->
-          errorlabstrm "field"
-            (str"cannot find a declared field structure for equality"++
-             spc()++str"\""++pr_constr req++str"\"")) *)
-
-let _ =
-  Summary.declare_summary "tactic-new-field-table"
-    { Summary.freeze_function =
-        (fun () -> !field_from_carrier,!field_from_relation,!field_from_name);
-      Summary.unfreeze_function =
-        (fun (ct,rt,nt) ->
-          field_from_carrier := ct; field_from_relation := rt;
-          field_from_name := nt);
-      Summary.init_function =
-        (fun () ->
-          field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty;
-          field_from_name := Spmap.empty) }
 
 let add_field_entry (sp,_kn) e =
-(*
-  let _ = ty e.field_ok in
-  let _ = ty e.field_simpl_eq_ok in
-  let _ = ty e.field_simpl_ok in
-  let _ = ty e.field_cond in
-*)
   field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier;
-  field_from_relation := Cmap.add e.field_req e !field_from_relation;
   field_from_name := Spmap.add sp e !field_from_name
 
 let subst_th (subst,th) =
@@ -987,10 +963,10 @@ let subst_th (subst,th) =
   let thm3' = subst_mps subst th.field_simpl_ok in
   let thm4' = subst_mps subst th.field_simpl_eq_in_ok in
   let thm5' = subst_mps subst th.field_cond in
-  let tac'= subst_tactic subst th.field_cst_tac in
-  let pow_tac' = subst_tactic subst th.field_pow_tac in
-  let pretac'= subst_tactic subst th.field_pre_tac in
-  let posttac'= subst_tactic subst th.field_post_tac in
+  let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in
+  let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in
   if c' == th.field_carrier &&
      eq' == th.field_req &&
      thm1' == th.field_ok &&
@@ -1019,17 +995,17 @@ let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
-      open_function = (fun i o -> if i=1 then cache_th o);
+      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x) }
 
-let field_equality r inv req =
+let field_equality evd r inv req =
   match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
-        mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
+    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
+        mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
     | _ ->
-	let _setoid = setoid_of_relation (Global.env ()) r req in
+	let _setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req)],Some(r,Some req) in
 	let inv_m, inv_m_lem =
 	  try Rewrite.default_morphism signature inv
@@ -1037,45 +1013,50 @@ let field_equality r inv req =
             error "field inverse should be declared as a morphism" in
 	  inv_m_lem
 
-let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv =
   check_required_library (cdir@["Field_tac"]);
   let env = Global.env() in
-  let sigma = Evd.empty in
+  let evd = ref sigma in
   let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
-    dest_field env sigma fth in
-  let (sth,ext) = build_setoid_params r add mul opp req eqth in
+    dest_field env evd fth in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
   let eqth = Some(sth,ext) in
-  let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign odiv in
-  let (pow_tac, pspec) = interp_power env power in
-  let sspec = interp_sign env sign in
-  let dspec = interp_div env odiv in
-  let inv_m = field_equality r inv req in
+  let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
+  let (pow_tac, pspec) = interp_power env evd power in
+  let sspec = interp_sign env evd sign in
+  let dspec = interp_div env evd odiv in
+  let inv_m = field_equality evd r inv req in
   let rk = reflect_coeff morphth in
-  let params =
-    exec_tactic env 9 (field_ltac"field_lemmas")
+  let params,ctx =
+    exec_tactic env !evd 9 (field_ltac"field_lemmas")
       (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in
-  let lemma1 = constr_of params.(3) in
-  let lemma2 = constr_of params.(4) in
-  let lemma3 = constr_of params.(5) in
-  let lemma4 = constr_of params.(6) in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
+  let lemma3 = params.(5) in
+  let lemma4 = params.(6) in
   let cond_lemma =
     match inj with
-      | Some thm -> mkApp(constr_of params.(8),[|thm|])
-      | None -> constr_of params.(7) in
-  let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in
-  let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in
-  let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
-  let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in
-  let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in
+      | Some thm -> mkApp(params.(8),[|thm|])
+      | None -> params.(7) in
+  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
+    ctx lemma1 in
+  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") 
+    ctx lemma2 in
+  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") 
+    ctx lemma3 in
+  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") 
+    ctx lemma4 in
+  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") 
+    ctx cond_lemma in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let posttac =
     match post with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
@@ -1092,9 +1073,9 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
           field_pre_tac = pretac;
           field_post_tac = posttac }) in  ()
 
-type field_mod =
-    Ring_mod of ring_mod
-  | Inject of Topconstr.constr_expr
+type 'constr field_mod =
+    Ring_mod of 'constr ring_mod
+  | Inject of Constrexpr.constr_expr
 
 VERNAC ARGUMENT EXTEND field_mod
   | [ ring_mod(m) ] -> [ Ring_mod m ]
@@ -1112,23 +1093,31 @@ let process_field_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_mod(Ring_kind k) -> set_once "field kind" kind k
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
     | Ring_mod(Const_tac t) ->
         set_once "tactic recognizing constants" cst_tac t
     | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
     | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
-    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext)
+    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
     | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
     | Ring_mod(Sign_spec t) -> set_once "sign" sign t
     | Ring_mod(Div_spec t) -> set_once "div" div t
-    | Inject i -> set_once "infinite property" inj (ic i)) l;
+    | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l;
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidField
+VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
   [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
+| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
+    msg_notice (strbrk "The following field structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.field_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.field_req))
+    ) !field_from_name ]
 END
 
 
@@ -1146,18 +1135,23 @@ let ltac_field_structure e =
   [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
-let field_lookup (f:glob_tactic_expr) lH rl t gl =
-  let env = pf_env gl in
-  let sigma = project gl in
-  let rl = make_args_list rl t in
-  let e = find_field_structure env sigma rl in
-  let rl = carg (make_term_list e.field_carrier rl) in
-  let lH = carg (make_hyp_list env lH) in
-  let field = ltac_field_structure e in
-  ltac_apply f (field@[lH;rl]) gl
+let field_lookup (f:glob_tactic_expr) lH rl t =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try
+      let evdref = ref sigma in
+      let rl = make_args_list rl t in
+      let e = find_field_structure env sigma rl in
+      let rl = carg (make_term_list env evdref e.field_carrier rl) in
+      let lH = carg (make_hyp_list env evdref lH) in
+      let field = ltac_field_structure e in
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = list_sep_last lt in field_lookup f lH l t ]
+      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
 END
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 580df9b5..595ba55e 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -7,7 +7,6 @@ InitialRing.vo
 NArithRing.vo
 RealField.vo
 Ring_base.vo
-Ring_equiv.vo
 Ring_polynom.vo
 Ring_tac.vo
 Ring_theory.vo