Changement dans ring et field, beaucoup de correction d'erreurs,

maintenant les differentes tactics marchent mieux mais le code
est moche ...



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

25 files changed, 705 insertions, 183 deletions

diff --git a/.depend.coq b/.depend.coq
index f8da6a1922..832ddc198e 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -38,7 +38,7 @@ theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories
 theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
 theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
 theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
 theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
 theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
@@ -154,7 +154,7 @@ theories/NArith/BinPos.vo: theories/NArith/BinPos.v
 theories/NArith/Pnat.vo: theories/NArith/Pnat.v theories/NArith/BinPos.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
 theories/NArith/BinNat.vo: theories/NArith/BinNat.v theories/NArith/BinPos.vo
 theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/NArithRing.vo
-theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo
+theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith_base.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo
 theories/NArith/Ndigits.vo: theories/NArith/Ndigits.v theories/Bool/Bool.vo theories/Bool/Bvector.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 theories/NArith/Ndec.vo: theories/NArith/Ndec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo theories/NArith/Nnat.vo theories/NArith/Ndigits.vo
 theories/NArith/Ndist.vo: theories/NArith/Ndist.v theories/Arith/Arith.vo theories/Arith/Min.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Ndigits.vo
@@ -285,7 +285,7 @@ theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories
 theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
 theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
 theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
 theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
 theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
@@ -372,7 +372,7 @@ contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid
 contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_polynom.vo
 contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo
 contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Ring_tac.vo
-contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo contrib/setoid_ring/Ring.vo
+contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo theories/NArith/BinNat.vo theories/NArith/Nnat.vo contrib/setoid_ring/Ring.vo
 contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v contrib/setoid_ring/Ring.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo
 contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 9015f3ce9d..074f6ef791 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -7,13 +7,32 @@
 (************************************************************************)
 
 Require Import Mult.
+Require Import BinNat.
+Require Import Nnat.
 Require Export Ring.
 Set Implicit Arguments.
 
+Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
+ Proof.
+  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
+  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
+  exact mult_plus_distr_r. 
+ Qed.
+
+Lemma nat_morph_N : 
+   semi_morph 0 1 plus mult (eq (A:=nat)) 
+          0%N 1%N Nplus Nmult Neq_bool nat_of_N.
+Proof.
+  constructor;trivial.
+  exact nat_of_Nplus.
+  exact nat_of_Nmult.
+  intros x y H;rewrite (Neq_bool_ok _ _ H);trivial.
+Qed.
+
 Ltac natcst t :=
   match isnatcst t with
-    true => t
-  | _ => NotConstant
+    true => constr:(N_of_nat t)
+  | _ => InitialRing.NotConstant
   end.
 
 Ltac Ss_to_add f acc :=
@@ -36,31 +55,6 @@ Ltac natprering :=
   | _ => idtac
   end.
 
- Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
- Proof.
-  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
-  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
-  exact mult_plus_distr_r. 
- Qed.
-
-
-Fixpoint nateq (n m:nat) {struct m} : bool :=
-  match n, m with
-  | O, O => true
-  | S n', S m' => nateq n' m'
-  | _, _ => false
-  end.
-
-Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m.
-Proof.
-  simple induction n; simple induction m; simpl; intros; try discriminate.
-  trivial.
-  rewrite (H n1 H1).
-  trivial.
-Qed.
-
 Add Ring natr : natSRth
-  (decidable nateq_ok, constants [natcst], preprocess [natprering]).
-
+  (morphism nat_morph_N, constants [natcst], preprocess [natprering]).
 
-(* Pourquoi on n'utilise pas N pour les calculs sur nat ???? *)
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index b2e693bc74..9e302df813 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -70,7 +70,7 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
 Ltac ParseFieldComponents lemma req :=
   match type of lemma with
   | context [
-        PCond _ _ _  _ _ _ _  _ _  _ _ ->
+     (*   PCond _ _ _  _ _ _ _  _ _  _ _ -> *)
         req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv 
                           ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
       (fun f => f radd rmul rsub ropp rdiv rinv rpow C)
@@ -93,7 +93,11 @@ Ltac fold_field_cond req :=
 
 Ltac simpl_PCond req :=
   protect_fv "field_cond";
-  try (exact I);
+  (try exact I);
+  fold_field_cond req.
+
+Ltac simpl_PCond_BEURK req :=
+  protect_fv "field_cond";
   fold_field_cond req.
 
 (* Rewriting (field_simplify) *)
@@ -129,32 +133,60 @@ Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl :=
   ParseFieldComponents lemma req Main.
 
 Ltac Field_simplify_gen f := 
-     fun req cst_tac pow_tac _ _ field_simplify_ok cond_ok pre post lH rl =>
+     fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl =>
        pre(); 
        Field_norm_gen f cst_tac pow_tac field_simplify_ok cond_ok req 
                   ring_subst_niter lH rl; 
       post().
 
 Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H).
-Ltac Field_simplify_in hyp:= 
-   Field_simplify_gen ltac:(fun H => rewrite H in hyp).
 
 Tactic Notation (at level 0) 
   "field_simplify" constr_list(rl) :=
-  field_lookup Field_simplify [] rl.
+  match goal with [|- ?G] => field_lookup Field_simplify [] rl [G] end.
 
 Tactic Notation (at level 0) 
   "field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
-  field_lookup Field_simplify [lH] rl.
+  match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end.
+
+Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=   
+ match goal with 
+ | [|- ?G] =>
+   let t := type of H in   
+   let g := fresh "goal" in
+   set (g:= G);
+   generalize H;clear H;
+   field_lookup Field_simplify [] rl [t];
+   intro H;
+   unfold g;clear g
+ end.
+
+Tactic Notation "field_simplify" "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=   
+ match goal with 
+ | [|- ?G] =>
+   let t := type of H in   
+   let g := fresh "goal" in
+   set (g:= G);
+   generalize H;clear H;
+   field_lookup Field_simplify [lH] rl [t];
+   intro H;
+   unfold g;clear g
+ end.
+
+(*
+Ltac Field_simplify_in hyp:= 
+   Field_simplify_gen ltac:(fun H => rewrite H in hyp).
 
 Tactic Notation (at level 0) 
   "field_simplify" constr_list(rl) "in" hyp(h) :=
-  field_lookup (Field_simplify_in h) [] rl.
+  let t := type of h in
+  field_lookup (Field_simplify_in h) [] rl [t].
 
 Tactic Notation (at level 0) 
   "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) :=
-  field_lookup (Field_simplify_in h) [lH] rl.
-
+  let t := type of h in
+  field_lookup (Field_simplify_in h) [lH] rl [t].
+*)
 
 (** Generic tactic for solving equations *)
 
@@ -193,7 +225,8 @@ Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH :=
          ltac:(fun ilemma =>
                   apply ilemma 
                   || fail "field anomaly: failed in applying lemma";
-                  [ Simpl_tac | apply Cond_lemma; simpl_PCond req]) in
+                  [ Simpl_tac | apply Cond_lemma; simpl_PCond req]);
+      clear vlpe nlemma in
     OnEquation req Main_eq in
   ParseFieldComponents lemma req Main.
 
@@ -202,34 +235,105 @@ Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH :=
 
 Ltac FIELD :=
    let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in
-   fun req cst_tac pow_tac field_ok _ _ cond_ok pre post lH rl =>
+   fun req cst_tac pow_tac field_ok _ _ _ cond_ok pre post lH rl =>
        pre(); 
        Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req 
-         Ring_tac.ring_subst_niter lH; 
+         Ring_tac.ring_subst_niter lH;
+       try exact I;
        post().
  
 Tactic Notation (at level 0) "field" :=
-  field_lookup FIELD [].
+  match goal with [|- ?G] => field_lookup FIELD [] [G] end.
 
 Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
-  field_lookup FIELD [lH].
+  match goal with [|- ?G] => field_lookup FIELD [lH] [G] end.
 
 (* transforms a field equation to an equivalent (simplified) ring equation,
    and leaves non-zero conditions to be proved (field_simplify_eq) *)
 Ltac FIELD_SIMPL  :=
   let Simpl := (protect_fv "field") in
-  fun req cst_tac pow_tac _ field_simplify_eq_ok _ cond_ok pre post lH rl =>
+  fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl =>
        pre(); 
        Field_Scheme Simpl cst_tac pow_tac field_simplify_eq_ok cond_ok 
           req Ring_tac.ring_subst_niter lH;
        post().
 
 Tactic Notation (at level 0) "field_simplify_eq" :=  
-  field_lookup FIELD_SIMPL [].
+  match goal with [|- ?G] => field_lookup FIELD_SIMPL [] [G] end.
 
 Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=  
-  field_lookup FIELD_SIMPL [lH].
+  match goal with [|- ?G] => field_lookup FIELD_SIMPL [lH] [G] end.
 
+(* Same as FIELD_SIMPL but in hypothesis *)
+
+Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH :=
+   let Main radd rmul rsub ropp rdiv rinv rpow C :=
+    let hyp := fresh "hyp" in
+    intro hyp;
+    match type of hyp with
+    | req ?t1 ?t2 =>
+      let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
+      let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
+      let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
+      let mkFE := 
+        mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
+      let rec ParseExpr ilemma :=
+        match type of ilemma with
+        |  forall nfe, ?fe = nfe -> _ =>
+          (fun t => 
+            let x := fresh "fld_expr" in 
+            let H := fresh "norm_fld_expr" in
+            compute_assertion H x fe;
+            ParseExpr (ilemma x H) t;
+            try clear H x)
+        | _ => (fun t => t ilemma)
+        end in
+      let fv := FV_hypo_tac mkFV req lH in
+      let fv := mkFFV t1 fv in
+      let fv := mkFFV t2 fv in
+      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+      let prh := proofHyp_tac lH in
+      let fe1 := mkFE t1 fv in
+      let fe2 := mkFE t2 fv in
+      let vlpe := fresh "vlpe" in
+      ParseExpr (lemma n fv lpe fe1 fe2 prh)
+         ltac:(fun ilemma =>
+             match type of ilemma with
+             | req _ _ ->  _ -> ?EQ => 
+               let tmp := fresh "tmp" in
+               assert (tmp : EQ);
+               [ apply ilemma; 
+                 [ exact hyp | apply Cond_lemma; simpl_PCond_BEURK req]
+               | protect_fv "field" in tmp;
+                 generalize tmp;clear tmp ];
+               clear hyp  
+             end)
+     end in
+  ParseFieldComponents lemma req Main.
+
+Ltac FIELD_SIMPL_EQ :=
+ fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl =>
+       pre(); 
+       Field_simplify_eq cst_tac pow_tac lemma cond_ok req
+         Ring_tac.ring_subst_niter lH;
+       post().
+
+Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
+  let t := type of H in
+  generalize H;
+  field_lookup FIELD_SIMPL_EQ [] [t];
+  [ try exact I
+  | clear H;intro H].
+
+
+Tactic Notation (at level 0) 
+  "field_simplify_eq" "[" constr_list(lH) "]"  "in" hyp(H) :=  
+  let t := type of H in
+  generalize H;
+  field_lookup FIELD_SIMPL_EQ [lH] [t];
+  [ try exact I
+  |clear H;intro H].
+ 
 (* Adding a new field *)
 
 Ltac ring_of_field f :=
@@ -258,6 +362,11 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec rk :=
      | None => constr:(Field_simplify_eq_correct)
      | Some _ => constr:(Field_simplify_eq_pow_correct)
      end in
+  let simpl_eq_in_lemma :=
+     match pspec with
+     | None => constr:(Field_simplify_eq_in_correct)
+     | Some _ => constr:(Field_simplify_eq_pow_in_correct)
+     end in
   let rw_lemma :=
      match pspec with
      | None => constr:(Field_rw_correct)
@@ -278,6 +387,11 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec rk :=
                    set ext_r inv_m afth 
                    _ _ _  _ _ _  _ _ _ morph 
                    _ _ _ pp_spec _ ss_spec) in
+       let field_simpl_eq_in :=
+         constr:(simpl_eq_in_lemma _ _ _  _ _ _  _ _ _ _
+                   set ext_r inv_m afth 
+                   _ _ _  _ _ _  _ _ _ morph 
+                   _ _ _ pp_spec _ ss_spec) in
        let field_ok := 
          constr:(Field_correct set ext_r inv_m afth morph pp_spec ss_spec) in
        let cond1_ok := 
@@ -285,9 +399,10 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec rk :=
        let cond2_ok := 
          constr:(Pcond_simpl_complete set ext_r afth morph pp_spec) in
        (fun f => 
-         f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok
+         f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
                 cond1_ok cond2_ok)
      | _ => fail 2 "bad sign specification"
      end 
      | _ => fail 1 "bad power specification" 
      end).
+
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 3da183d5a4..0c7f235120 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -107,8 +107,8 @@ Hint Resolve (ARadd_0_l  ARth) (ARadd_comm  ARth) (ARadd_assoc ARth)
 Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
 Notation Nnorm := (norm_subst cO cI cadd cmul csub copp ceqb).
 
-Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI copp ceqb phi get_sign).
-Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI copp ceqb phi Cp_phi rpow get_sign).
+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).
@@ -990,7 +990,6 @@ Eval compute
  Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0.
 Proof.
  induction p;simpl.
-  rewrite <- ARth.(ARmul_assoc).
   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). rewrite H1. rewrite Hp;ring. ring.
@@ -1152,8 +1151,9 @@ 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).
-intro Hp;apply (pow_pos_not_0 Hdiff  p). rewrite  (@rmul_reg_l _ (pow_pos rmul r0 p)  0 Hdiff).
-rewrite Hp;ring. reflexivity.
+intro Hp;apply (pow_pos_not_0 Hdiff  p). 
+rewrite  (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p)  0).
+ apply pow_pos_not_0;trivial. ring [Hp]. reflexivity.
 apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
 rewrite IHp;reflexivity.
 rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
@@ -1352,6 +1352,107 @@ rewrite Hcrossprod in |- *.
 reflexivity.
 Qed.
 
+Theorem Field_simplify_eq_pow_in_correct :
+ forall 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 ->
+ 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 ->
+ FEeval l fe1 == FEeval l fe2 ->
+  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. 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. 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_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+Qed.
+
+Theorem Field_simplify_eq_in_correct :
+forall 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 ->
+ 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 ->
+ FEeval l fe1 == FEeval l fe2 ->
+  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. 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. 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_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+Qed.
+
+
 Section Fcons_impl.
 
 Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C).
@@ -1750,4 +1851,3 @@ Qed.
 End Field.
 
 End Complete.
-
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index a456f47799..bbdcd44330 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -484,6 +484,7 @@ Ltac gen_ring_sign set rspec morph sspec rk :=
  | Some ?t => constr:(t)
  end.
 
+
 Ltac ring_elements set ext rspec pspec sspec rk :=
   let arth := coerce_to_almost_ring set ext rspec in
   let ext_r := coerce_to_ring_ext ext in
@@ -496,17 +497,21 @@ Ltac ring_elements set ext rspec pspec sspec rk :=
             constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
         | _ => fail 2 "ring anomaly"
         end
-    | @Morphism ?m => m
+    | @Morphism ?m =>
+       match type of m with 
+       | ring_morph _ _ _ _ _ _ _  _ _ _ _ _ _  _ _ => m 
+       | @semi_morph _ _ _ _ _ _  _ _ _ _ _  _ _   => 
+           constr:(SRmorph_Rmorph set m) 
+       | _ => fail 2 " ici"
+       end
     | _ => fail 1 "ill-formed ring kind"
     end in
   let p_spec := gen_ring_pow set arth pspec in
   let s_spec := gen_ring_sign set rspec morph sspec rk in
   fun f => f arth ext_r morph p_spec s_spec.
 
-
 (* Given a ring structure and the kind of morphism,
    returns 2 lemmas (one for ring, and one for ring_simplify). *)
-
 Ltac ring_lemmas set ext rspec pspec sspec rk :=
   let gen_lemma2 :=
     match pspec with
diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index 92fbc1b587..106bb793dc 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -115,7 +115,7 @@ Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R))  nat_of_N pow.
 Proof.
  constructor. destruct n. reflexivity.
  simpl. induction p;simpl. 
- rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. symmetry; apply Rmult_assoc.
+ rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity.
  unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial.
  rewrite Rmult_comm;apply Rmult_1_l.
 Qed.
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index f2c8a460cd..8567037d91 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -324,7 +324,34 @@ Section MakeRingPol.
    end.
  
  End PmulI.
+(* A symmetric version of the multiplication *)
 
+ Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
+   match P'' with
+   | Pc c => PmulC P c
+   | Pinj j' Q' => PmulI Pmul Q' j' P
+   | PX P' i' Q' =>
+     match P with
+     | Pc c => PmulC P'' c
+     | Pinj j Q =>
+       let QQ' := 
+         match j with
+         | xH => Pmul Q Q'
+         | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q' 
+         | xI j => Pmul (Pinj (xO j) Q) Q'
+         end in
+       mkPX (Pmul P P') i' QQ'
+     | PX P i Q=>
+       let QQ' := Pmul Q Q' in
+       let PQ' := PmulI Pmul Q' xH P in
+       let QP' := Pmul (mkPinj xH Q) P' in
+       let PP' := Pmul P P' in
+       (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ'
+     end
+  end.    
+
+(* Non symmetric *)
+(*       
  Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol :=
   match P' with
   | Pc c' => PmulC P c'
@@ -338,11 +365,21 @@ Section MakeRingPol.
   | Pc c => PmulC P' c
   | Pinj j Q => PmulI Pmul_aux Q j P'
   | PX P i Q => 
-    Padd (mkPX (Pmul_aux P P') i P0) (PmulI Pmul_aux Q xH P')
+    (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P')
   end.
+*)
  Notation "P ** P'" := (Pmul P P').
- 
- 
+
+ Fixpoint Psquare (P:Pol) : Pol :=
+   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 **)
      
@@ -710,7 +747,34 @@ Section MakeRingPol.
   rewrite H;rewrite Pplus_comm.
   rewrite pow_pos_Pplus;rsimpl.
  Qed.
- 
+(* Proof for the symmetriv version *)
+
+ Lemma PmulI_ok : 
+  forall P', 
+   (forall (P : Pol) (l : list R), (Pmul P P') @ l == P @ l * P' @ l) ->
+   forall (P : Pol) (p : positive) (l : list R),
+    (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
+ Proof.
+  induction P;simpl;intros.
+  Esimpl2;apply (ARmul_comm ARth).
+  assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
+  rewrite H1; rewrite H;rrefl.
+  rewrite H1; rewrite H.
+  rewrite Pplus_comm.
+  rewrite jump_Pplus;simpl;rrefl.
+  rewrite H1;rewrite Pplus_comm.
+  rewrite jump_Pplus;rewrite IHP;rrefl.
+  destruct p0;Esimpl2.
+  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
+  mul_push (pow_pos rmul (hd 0 l) p);rrefl.
+  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
+  mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
+  rewrite IHP1;simpl;rsimpl.
+  mul_push (pow_pos rmul (hd 0 l) p).
+  rewrite H;rrefl.
+ Qed.
+
+(*
  Lemma PmulI_ok : 
   forall P', 
    (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) ->
@@ -744,9 +808,33 @@ Section MakeRingPol.
   rewrite Padd_ok;Esimpl2.
   rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl.
  Qed.
+*)
 
+(* Proof for the symmetric version *)
  Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
  Proof.
+  intros P P';generalize P;clear P;induction P';simpl;intros.
+  apply PmulC_ok. apply PmulI_ok;trivial.
+  destruct P.
+  rewrite (ARmul_comm ARth);Esimpl2;Esimpl2.
+  Esimpl2. rewrite IHP'1;Esimpl2.
+   assert (match p0 with
+           | xI j => Pinj (xO j) P ** P'2
+           | xO j => Pinj (Pdouble_minus_one j) P ** P'2 
+           | 1 => P ** P'2
+           end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)).
+   destruct p0;simpl;rewrite IHP'2;Esimpl.
+   rewrite jump_Pdouble_minus_one;Esimpl.
+   rewrite H;Esimpl.
+   rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2.
+   repeat (rewrite IHP'1 || rewrite IHP'2);simpl.
+   rewrite PmulI_ok;trivial.
+   mul_push (P'1@l). simpl. mul_push (P'2 @ (tail l)). Esimpl.
+ Qed.
+
+(*
+Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+ Proof.
   destruct P;simpl;intros.
   Esimpl2;apply (ARmul_comm ARth).
   rewrite (PmulI_ok P (Pmul_aux_ok P)).
@@ -756,6 +844,16 @@ Section MakeRingPol.
   rewrite Pmul_aux_ok;mul_push (P' @ l).
   rewrite (ARmul_comm ARth (P' @ l));rrefl.
  Qed.
+*)
+
+ Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
+ Proof.
+  induction P;simpl;intros;Esimpl2.
+  apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2.
+  rewrite IHP1;rewrite IHP2.
+  mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l).
+  rrefl.
+ Qed.
 
 
  Lemma mkZmon_ok: forall M j l,
@@ -869,8 +967,11 @@ Section MakeRingPol.
        rewrite (Pplus_minus _ _ He); rsimpl.
  Qed.
 
+(* Proof for the symmetric version *)
+
  Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
     POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ Proof.
  intros P2 M1 P3 P4 l; unfold POneSubst.
  generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
  intros Q1 R1; case R1.
@@ -881,16 +982,40 @@ Section MakeRingPol.
    discriminate.
    intros _ H1 H2; injection H1; intros; subst.
    rewrite H2; rsimpl.
-   rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
+ (* new version *)
+   rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
  intros i P5 H; rewrite H.
    intros HH H1; injection HH; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite Pmul_ok; rewrite H1; rsimpl.
+   rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl.
  intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
-   injection H2; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
+   assert (P4 = Q1 ++ P3 ** PX i P5 P6).
+   injection H2; intros; subst;trivial.
+  rewrite H;rewrite Padd_ok;rewrite Pmul_ok;rsimpl.
  Qed.
-
-
+(*
+  Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
+    POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+Proof.
+ intros P2 M1 P3 P4 l; unfold POneSubst.
+ generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
+ intros Q1 R1; case R1.
+   intros c H; rewrite H.
+   generalize (morph_eq CRmorph c cO);
+        case (c ?=! cO); simpl; auto.
+   intros H1 H2; rewrite H1; auto; rsimpl.
+   discriminate.
+   intros _ H1 H2; injection H1; intros; subst.
+   rewrite H2; rsimpl.
+  rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
+  intros i P5 H; rewrite H.
+   intros HH H1; injection HH; intros; subst; rsimpl.
+   rewrite Padd_ok; rewrite Pmul_ok. rewrite H1; rsimpl.
+   intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
+   injection H2; intros; subst; rsimpl.
+   rewrite Padd_ok.
+   rewrite Pmul_ok; rsimpl.
+ Qed. 
+*)
  Lemma PNSubst1_ok: forall n P1 M1 P2 l,
     Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
  Proof.
@@ -999,6 +1124,66 @@ Section MakeRingPol.
   | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l)
   end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). 
 
+(* Power using the chinise algorithm *)
+(*Section POWER.
+  Variable subst_l : Pol -> Pol.
+  Fixpoint Ppow_pos (P:Pol) (p:positive){struct p} : Pol :=
+   match p with
+   | xH => P
+   | xO p => subst_l (Psquare (Ppow_pos P p))
+   | xI p => subst_l (Pmul P (Psquare (Ppow_pos P p)))
+   end.
+ 
+  Definition Ppow_N P n :=
+   match n with
+   | N0 => P1
+   | Npos p => Ppow_pos P p
+   end.
+ 
+  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
+         forall P p, (Ppow_pos P p)@l == (pow_pos Pmul P p)@l.
+  Proof.
+   intros l subst_l_ok P.
+   induction p;simpl;intros;try rrefl;try rewrite subst_l_ok.
+   repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl.
+   repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl.
+  Qed.
+ 
+  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
+         forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
+  Proof.  destruct n;simpl. rrefl. apply Ppow_pos_ok. trivial.  Qed.
+    
+ End POWER. *)
+
+Section POWER.
+  Variable subst_l : Pol -> Pol.
+  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
+   match p with
+   | xH => subst_l (Pmul res P) 
+   | xO p => Ppow_pos (Ppow_pos res P p) P p
+   | xI p => subst_l (Pmul  (Ppow_pos (Ppow_pos res P p) P p) P)
+   end.
+ 
+  Definition Ppow_N P n :=
+   match n with
+   | N0 => P1
+   | Npos p => Ppow_pos P1 P p
+   end.
+ 
+  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
+         forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l.
+  Proof.
+   intros l subst_l_ok res P p. generalize res;clear res.
+   induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp.
+   rsimpl. mul_push (P@l);rsimpl. rsimpl. rrefl.
+  Qed.
+ 
+  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
+         forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
+  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl.  Qed.
+    
+ End POWER.
+
  (** Normalization and rewriting *)
 
  Section NORM_SUBST_REC.
@@ -1006,7 +1191,8 @@ Section MakeRingPol.
   Variable lmp:list (Mon*Pol).
   Let subst_l P := PNSubstL P lmp n n.
   Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
-
+  Let Ppow_subst := Ppow_N subst_l. 
+  
   Fixpoint norm_subst (pe:PExpr) : Pol :=
    match pe with
    | PEc c => Pc c
@@ -1018,7 +1204,7 @@ Section MakeRingPol.
    | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2)
    | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2) 
    | PEopp pe1 => Popp (norm_subst pe1)
-   | PEpow pe1 n => pow_N P1 Pmul_subst (norm_subst pe1) n
+   | PEpow pe1 n => Ppow_subst (norm_subst pe1) n
    end.
 
   Lemma norm_subst_spec : 
@@ -1036,8 +1222,10 @@ Section MakeRingPol.
    rewrite IHpe1;rewrite IHpe2;rrefl.
    rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl.
    rewrite IHpe;rrefl.
+   unfold Ppow_subst. rewrite Ppow_N_ok. trivial.
    rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
-   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;rrefl.
+   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
+      repeat rewrite Pmul_ok;rrefl.
   Qed.
 
  End NORM_SUBST_REC.
@@ -1176,8 +1364,12 @@ Section MakeRingPol.
    else mkmult_rec [c] (rev' lm).
 
   Definition mkmult_c c lm :=
-   if c ?=! copp cI then mkmultm1 (rev' lm)
-   else mkmult_c_pos c lm.
+   match get_sign c with
+   | None => mkmult_c_pos c lm
+   | Some c' => 
+     if c' ?=! cI then mkmultm1 (rev' lm)
+     else mkmult_rec [c] (rev' lm)
+   end.
       
   Definition mkadd_mult rP c lm :=
    match get_sign c with
@@ -1272,11 +1464,15 @@ Section MakeRingPol.
  Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm.
  Proof.
   intros;unfold mkmult_c;simpl.
-  assert (H := (morph_eq CRmorph) c (copp cI)).
-  destruct (c ?=! copp cI). 
-  rewrite <- r_list_pow_rev;rewrite H;trivial;Esimpl.
-  apply mkmultm1_ok. apply mkmult_c_pos_ok.
- Qed.
+  case_eq (get_sign c);intros.
+  assert (H1 := (morph_eq CRmorph) c0  cI).
+  destruct (c0 ?=! cI).
+   rewrite (get_sign_spec.(sign_spec) _ H). rewrite H1;trivial.
+   rewrite <- r_list_pow_rev;trivial;Esimpl.
+  apply mkmultm1_ok.
+ rewrite <- r_list_pow_rev; apply mkmult_rec_ok.
+ apply mkmult_c_pos_ok.
+Qed.
 
  Lemma mkadd_mult_ok : forall rP c lm, mkadd_mult rP c lm == rP + [c]*r_list_pow lm.
  Proof.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index d9d82aa0a3..fbaff6e882 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -60,7 +60,7 @@ Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
    (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
    clear H;
    OnMainSubgoal Heq ltac:(type of Heq)
-     ltac:(try tac Heq; clear Heq npe; CONT_tac cont_arg)).
+     ltac:(try tac Heq; clear Heq npe;CONT_tac cont_arg)).
 
 (* General scheme of reflexive tactics using of correctness lemma
    that involves normalisation of one expression *)
@@ -69,7 +69,7 @@ Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms :=
   (* extend the atom list *)
   let fv := list_fold_left FV_tac fv terms in
   let RW_tac lemma := 
-    let fcons term CONT_tac cont_arg := 
+     let fcons term CONT_tac cont_arg := 
       let expr := SYN_tac term fv in
       (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in
      (* rewrite steps *)
@@ -227,18 +227,15 @@ Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
     ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in
   ParseRingComponents lemma2 Main.
 
-Ltac Ring_gen pre post cst_tac pow_tac lemma1 req lH :=
-  pre(); Ring cst_tac pow_tac lemma1 req ring_subst_niter lH.
+Ltac Ring_gen
+  req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl :=
+  pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH.
 
 Tactic Notation (at level 0) "ring" :=
-  ring_lookup
-    (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
-       Ring_gen pre post cst_tac pow_tac lemma1 req lH) [].
+  match goal with [|- ?G] => ring_lookup Ring_gen [] [G] end.
 
 Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
-  ring_lookup
-    (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
-       pre(); Ring_gen pre post cst_tac pow_tac lemma1 req lH) [lH].
+  match goal with [|- ?G] => ring_lookup Ring_gen [lH] [G] end.
 
 (* Simplification *)
 
@@ -250,22 +247,112 @@ Ltac Ring_simplify_gen f :=
      post().
 
 Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
+
+
+Tactic Notation (at level 0) 
+  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := 
+  match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end.
+
+Tactic Notation (at level 0) 
+  "ring_simplify" constr_list(rl) := 
+  match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end.
+
+(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
+
+Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=   
+ match goal with 
+ | [|- ?G] =>
+   let t := type of H in   
+   let g := fresh "goal" in
+   set (g:= G);
+   generalize H;clear H;
+   ring_lookup Ring_simplify [] rl [t];
+   intro H;
+   unfold g;clear g
+ end.
+
+Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=   
+ match goal with 
+ | [|- ?G] =>
+   let t := type of H in   
+   let g := fresh "goal" in
+   set (g:= G);
+   generalize H;clear H;
+   ring_lookup Ring_simplify [lH] rl [t];
+   intro H;
+   unfold g;clear g
+ end.
+
+
+(*     LE RESTE MARCHE PAS DOMAGE  .....  *)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+(*
+
+
+
+
+
+
+
+
 Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp).
 
 
 Tactic Notation (at level 0) 
   "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := 
-  ring_lookup Ring_simplify [lH] rl.
+  match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end.
 
 Tactic Notation (at level 0) 
   "ring_simplify" constr_list(rl) := 
-  ring_lookup Ring_simplify [] rl.
+  match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end.
 
 Tactic Notation (at level 0) 
   "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= 
-  ring_lookup (Ring_simplify_in h) [lH] rl.
+  let t := type of h in
+  ring_lookup 
+   (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
+     pre(); 
+     Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
+     post()) 
+  [lH] rl [t]. 
+(*  ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *)
+
+Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp).
 
 Tactic Notation (at level 0) 
-  "ring_simplify" constr_list(rl) "in" hyp(h):= 
-  ring_lookup (Ring_simplify_in h) [] rl.
+  "ring_simplify" constr_list(rl) "in" constr(h):= 
+  let t := type of h in
+  ring_lookup   
+   (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
+     pre(); 
+     Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
+     post())
+ [] rl [t].
+
+Ltac rw_in H Heq := rewrite Heq in H.
+
+Ltac simpl_in H := 
+  let t := type of H in
+   ring_lookup 
+   (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
+     pre(); 
+     Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
+     post()) 
+   [] [t].
+
 
+*)
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index dd63cf6d59..5498911d08 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -51,16 +51,16 @@ Section Power.
   match i with
   | xH => x
   | xO i => let p := pow_pos x i in rmul p p
-  | xI i => let p := pow_pos x i in rmul (rmul x p) p
+  | xI i => let p := pow_pos x i in rmul x (rmul p p)
   end.
 
  Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
  Proof.
   induction j;simpl.
-  rewrite IHj. 
+  rewrite IHj.
+  rewrite (mul_comm x (pow_pos x j *pow_pos x j)).
   set (w:= x*pow_pos x j);unfold w at 2.
   rewrite (mul_comm x (pow_pos x j));unfold w.
-  rewrite (mul_comm x (x * pow_pos x j * pow_pos x j)).
   repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
   repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
   apply (Seq_refl _ _ Rsth).
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 56367bc139..8de7021e84 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -54,7 +54,3 @@ Add Ring Zr : Zth
   (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
    power_tac Zpower_theory [Zpow_tac]).
 
-
-
-
-
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index c22f1eb174..5140b3bf02 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -217,15 +217,19 @@ let coq_Some = coq_constant "Some"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
+let dest_rel0 t =  
+  match kind_of_term t with
+  | App(f,args) when Array.length args >= 2 ->
+      let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
+      if closed0 rel then
+        (rel,args.(Array.length args - 2),args.(Array.length args - 1))
+      else error "ring: cannot find relation (not closed)"
+  | _ -> error "ring: cannot find relation"
+
 let rec dest_rel t =
   match kind_of_term t with
-      App(f,args) when Array.length args >= 2 ->
-        let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
-        if closed0 rel then
-          (rel,args.(Array.length args - 2),args.(Array.length args - 1))
-        else error "ring: cannot find relation (not closed)"
-    | Prod(_,_,c) -> dest_rel c
-    | _ -> error "ring: cannot find relation"
+  | Prod(_,_,c) -> dest_rel c
+  | _ -> dest_rel0 t
 
 (****************************************************************************)
 (* Library linking *)
@@ -299,9 +303,9 @@ let _ = add_map "ring"
     coq_nil, (function -1->Eval|_ -> Prot);
     (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
-    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|13|15->Eval|14->Rec|_->Prot);
+    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
     pol_cst "Pphi_pow", 
-          (function -1|8|9|10|11|12|14|16|18->Eval|17->Rec|_->Prot);
+          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring 
        operations and make recursive call on the var map *)
     pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)])
@@ -335,7 +339,7 @@ let ring_lookup_by_name ref =
   Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name
 
 
-let find_ring_structure env sigma l cl oname =
+let find_ring_structure env sigma l oname =
   match oname, l with
       Some rf, _ ->
         (try ring_lookup_by_name rf
@@ -356,13 +360,14 @@ let find_ring_structure env sigma l cl oname =
           errorlabstrm "ring"
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
-    | None, [] ->
+    | None, [] -> 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"\""))
+             spc()++str"\""++pr_constr req++str"\"")) *)
 
 let _ = 
   Summary.declare_summary "tactic-new-ring-table"
@@ -688,21 +693,23 @@ END
 (* The tactics consist then only in a lookup in the ring database and
    call the appropriate ltac. *)
 
-let make_term_list carrier rl gl =
-  let rl = 
-    match rl with
-	[] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2]
-      | _ -> rl in
+let make_args_list rl t = 
+  match rl with
+  | [] -> 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 ring_lookup (f:glob_tactic_expr) lH rl gl =
+let ring_lookup (f:glob_tactic_expr) lH rl t gl =
   let env = pf_env gl in
   let sigma = project gl in
-  let e = find_ring_structure env sigma rl (pf_concl gl) None in
-  let rl = carg (make_term_list e.ring_carrier rl gl) in
+  let rl = make_args_list rl t in
+  let e = find_ring_structure env sigma rl None in
+  let rl = carg (make_term_list e.ring_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let req = carg e.ring_req in
   let sth = carg e.ring_setoid in
@@ -723,8 +730,9 @@ let ring_lookup (f:glob_tactic_expr) lH rl gl =
           lemma1;lemma2;pretac;posttac;lH;rl])) gl
 
 TACTIC EXTEND ring_lookup
-| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)] ->
-          [ring_lookup (fst f) lH lr]
+| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)
+      "[" constr(t) "]" ] ->
+          [ring_lookup (fst f) lH lr t]
 END
 
 
@@ -745,14 +753,14 @@ let _ = add_map "field"
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
     my_constant "display_linear",
-      (function -1|8|9|10|11|12|13|14|16|17->Eval|15->Rec|_->Prot);
+      (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
     my_constant "display_pow_linear",
-     (function -1|8|9|10|11|12|13|14|15|17|19|20->Eval|18->Rec|_->Prot);
+     (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 *)
-    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|13|15->Eval|14->Rec|_->Prot);
+    pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
     pol_cst "Pphi_pow", 
-          (function -1|8|9|10|11|12|14|16|18->Eval|17->Rec|_->Prot);
+          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring 
        operations and make recursive call on the var map *)
     pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
@@ -805,6 +813,7 @@ type field_info =
       field_ok : constr;
       field_simpl_eq_ok : constr;
       field_simpl_ok : constr;
+      field_simpl_eq_in_ok : constr;
       field_cond : constr;
       field_pre_tac : glob_tactic_expr;
       field_post_tac : glob_tactic_expr }
@@ -821,7 +830,7 @@ let field_lookup_by_name ref =
     !field_from_name
 
 
-let find_field_structure env sigma l cl oname =
+let find_field_structure env sigma l oname =
   check_required_library (cdir@["Field_tac"]);
   match oname, l with
       Some rf, _ ->
@@ -843,13 +852,13 @@ let find_field_structure env sigma l cl oname =
           errorlabstrm "field"
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
-    | None, [] ->
-        let (req,_,_) = dest_rel cl in
+    | None, [] -> 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"\""))
+             spc()++str"\""++pr_constr req++str"\"")) *)
 
 let _ = 
   Summary.declare_summary "tactic-new-field-table"
@@ -883,7 +892,8 @@ let subst_th (_,subst,th) =
   let thm1' = subst_mps subst th.field_ok in
   let thm2' = subst_mps subst th.field_simpl_eq_ok in
   let thm3' = subst_mps subst th.field_simpl_ok in
-  let thm4' = subst_mps subst th.field_cond 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
@@ -893,7 +903,8 @@ let subst_th (_,subst,th) =
      thm1' == th.field_ok &&
      thm2' == th.field_simpl_eq_ok &&
      thm3' == th.field_simpl_ok &&
-     thm4' == th.field_cond &&
+     thm4' == th.field_simpl_eq_in_ok &&
+     thm5' == th.field_cond &&
      tac' == th.field_cst_tac &&
      pow_tac' == th.field_pow_tac &&
      pretac' == th.field_pre_tac &&
@@ -906,7 +917,8 @@ let subst_th (_,subst,th) =
       field_ok = thm1';
       field_simpl_eq_ok = thm2';
       field_simpl_ok = thm3';
-      field_cond = thm4';
+      field_simpl_eq_in_ok = thm4';
+      field_cond = thm5';
       field_pre_tac = pretac';
       field_post_tac = posttac' }
 
@@ -953,19 +965,21 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
   let inv_m = default_field_equality r inv req in
   let rk = reflect_coeff morphth in
   let params =
-    exec_tactic env 8 (field_ltac"field_lemmas")
+    exec_tactic env 9 (field_ltac"field_lemmas")
       (List.map carg[sth;ext;inv_m;fth;pspec;sspec;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 cond_lemma =
     match inj with
-      | Some thm -> mkApp(constr_of params.(7),[|thm|])
-      | None -> constr_of params.(6) in
+      | 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 cond_lemma = decl_constant (string_of_id name^"_lemma4") cond_lemma 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
   let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
@@ -985,6 +999,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
           field_ok = lemma1;
           field_simpl_eq_ok = lemma2;
           field_simpl_ok = lemma3;
+          field_simpl_eq_in_ok = lemma4;
           field_cond = cond_lemma;
           field_pre_tac = pretac;
           field_post_tac = posttac }) in  ()
@@ -1026,11 +1041,12 @@ VERNAC COMMAND EXTEND AddSetoidField
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign]
 END
 
-let field_lookup (f:glob_tactic_expr) lH rl gl =
+let field_lookup (f:glob_tactic_expr) lH rl t gl =
   let env = pf_env gl in
   let sigma = project gl in
-  let e = find_field_structure env sigma rl (pf_concl gl) None in
-  let rl = carg (make_term_list e.field_carrier rl gl) in
+  let rl = make_args_list rl t in
+  let e = find_field_structure env sigma rl None in
+  let rl = carg (make_term_list e.field_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let req = carg e.field_req in
   let cst_tac = Tacexp e.field_cst_tac in
@@ -1038,6 +1054,7 @@ let field_lookup (f:glob_tactic_expr) lH rl gl =
   let field_ok = carg e.field_ok in
   let field_simpl_ok = carg e.field_simpl_ok in
   let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
+  let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in
   let cond_ok = carg e.field_cond in
   let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in
   let posttac = Tacexp(TacFun([None],e.field_post_tac)) in
@@ -1045,10 +1062,11 @@ let field_lookup (f:glob_tactic_expr) lH rl gl =
     (TacLetIn
       ([(dummy_loc,id_of_string"f"),None,Tacexp f],
        ltac_lcall "f"
-        [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok;
-         pretac;posttac;lH;rl])) gl
+        [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
+         field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl
 
 TACTIC EXTEND field_lookup
-| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) ] -> 
-      [ field_lookup (fst f) lH l ]
+| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) 
+     "[" constr(t) "]" ] -> 
+      [ field_lookup (fst f) lH l t ]
 END
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index c0087bd300..5465bc692e 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Compare_dec.
 Require Import Sumbool.
 Require Import Div2.
@@ -174,4 +174,4 @@ Proof.
   pattern n at 1; rewrite <- (nat_of_N_of_nat n).
   pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
   symmetry; apply nat_of_Ncompare.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 060de9a447..51ed8a4c05 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -92,9 +92,9 @@ Proof.
     replace (Un (S (2 * S N)) + (-1 * Un (S (2 * S N)) + Un (S (S (2 * S N)))))
       with (Un (S (S (2 * S N)))); [ idtac | ring ].
   apply H.
-  ring_nat.
+  ring.
   apply HrecN.
-  ring_nat.
+  ring.
 Qed.
 
 (** A more general inequality *)
@@ -300,7 +300,7 @@ Proof.
   do 2 rewrite Rmult_1_r; apply le_INR.
   replace (2 * S n + 1)%nat with (S (S (2 * n + 1))).
   apply le_trans with (S (2 * n + 1)); apply le_n_Sn.
-  ring_nat.
+  ring.
   apply not_O_INR; discriminate.
   apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
     [ discriminate | ring ].
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index eab47da8e0..a5c5ddaf82 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -75,7 +75,7 @@ Proof.
   apply H3; assumption.
   right.
   apply H4; assumption.
-  unfold double in |- *; ring.
+  unfold double in |- *;ring.
 Qed.
 
   (* 2m <= 2n => m<=n *)
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 82b0a3949d..1ef4f1ec4d 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -486,7 +486,7 @@ Proof.
   apply le_trans with (pred N).
   assumption.
   apply le_pred_n.
-  ring_nat.
+  ring.
   apply Rle_trans with
     (sum_f_R0
       (fun k:nat =>
@@ -515,7 +515,7 @@ Proof.
   apply le_trans with (2 * S (S (n0 + n)))%nat.
   replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   omega.
   right.
   unfold Rdiv in |- *; rewrite Rmult_comm.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 23d24bdf26..a79b74d7b7 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -87,7 +87,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -96,7 +96,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -367,7 +367,7 @@ Proof.
   apply le_trans with (pred N).
   apply H0.
   apply le_pred_n.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   cut (S N = (2 * S N0)%nat).
   intro.
   replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -388,7 +388,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   unfold C, Rdiv in |- *.
   rewrite (Rmult_comm (INR (fact (S N)))).
   rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -494,7 +494,7 @@ Proof.
   simpl in |- *.
   pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
     apply Rlt_0_1.
-  ring_nat.
+  ring.
   unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0.
   unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate.
   assert (H0 := even_odd_cor N).
@@ -515,7 +515,7 @@ Proof.
   replace (S (S (2 * N0))) with (2 * S N0)%nat.
   do 2 rewrite div2_double.
   reflexivity.
-  ring_nat.
+  ring.
   apply S_pred with 0%nat; apply H.
 Qed.
 
@@ -585,8 +585,8 @@ Proof.
   apply (fun m n p:nat => mult_le_compat_l p n m).
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   reflexivity.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
@@ -623,7 +623,7 @@ Proof.
   replace (2 * N1)%nat with (S (S (2 * pred N1))).
   reflexivity.
   pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
-  ring_nat.
+  ring.
   symmetry  in |- *; apply S_pred with 0%nat; apply H8.
   apply INR_lt.
   apply Rmult_lt_reg_l with (INR 2).
@@ -641,7 +641,7 @@ Proof.
   rewrite div2_double.
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   reflexivity.
   apply le_trans with (max (2 * S N0) 2).
   apply le_max_l.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 72b9aee32b..6692fd8c7a 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -278,7 +278,7 @@ Proof.
   rewrite (tech5 An (2 * S N)).
   rewrite <- HrecN.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma sum_Rle :
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index daebd91789..5d13275281 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,6 +13,8 @@
 (***************************************************************************)
 
 Require Export Raxioms.
+Require Import Rpow_def.
+Require Import Zpower.
 Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
@@ -1528,6 +1530,16 @@ Proof.
   rewrite Rmult_opp_opp; auto with real.
 Qed.
 
+Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
+Proof.
+ intros z [|n];simpl;trivial.
+ rewrite Zpower_pos_nat.
+ rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
+ rewrite mult_IZR.
+ induction n;simpl;trivial.
+ rewrite mult_IZR;ring[IHn].
+Qed.
+
 (**********)
 Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index ba7396ed61..54bc50e0aa 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -15,7 +15,6 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
-Require Export LegacyArithRing. (* for ring_nat... *)
 Require Export ArithRing.
 
 Require Import Rbase.
@@ -378,7 +377,7 @@ Proof.
   replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
   rewrite Hrecn; reflexivity.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
@@ -425,7 +424,7 @@ Proof.
   rewrite Hrecn2.
   simpl in |- *.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 6af9916730..9175927029 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -53,7 +53,7 @@ Section Sigma.
     apply lt_minus_O_lt; assumption.
     apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     replace (high - S (S k))%nat with (high - S k - 1)%nat.
     apply pred_of_minus.
     omega.
@@ -71,7 +71,7 @@ Section Sigma.
     apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
     apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     omega.
     inversion H; [ right; reflexivity | left; assumption ].
   Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 70fb3e6d0e..14359574f8 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -522,7 +522,7 @@ Proof.
   intro; assumption.
   intro; reflexivity.
   split.
-  intro; elim diff_false_true; assumption.
+  intro feqt;discriminate feqt.
   intro.
   elim n0; assumption.
   unfold Vn in |- *.
@@ -540,7 +540,7 @@ Proof.
   unfold cond_positivity in |- *.
   case (Rle_dec 0 z); intro.
   split.
-  intro; elim diff_true_false; assumption.
+  intro feqt; discriminate feqt.
   intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
   split.
   intro; auto with real.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 2adac468bf..2f69fb7616 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -466,10 +466,10 @@ Proof.
   unfold x in |- *; replace 0 with (INR 0);
     [ apply le_INR; apply le_O_n | reflexivity ].
   prove_sup0.
-  ring_nat.
+  ring.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 57878b61f7..d6ab9a4ce7 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -121,7 +121,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   assert (H3 := cv_speed_pow_fact a); unfold Un in |- *; unfold Un_cv in H3;
     unfold R_dist in H3; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros; elim (H3 eps H4); intros N H5.
@@ -316,7 +316,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   assert (H4 := cv_speed_pow_fact a0); unfold Un in |- *; unfold Un_cv in H4;
     unfold R_dist in H4; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros; elim (H4 eps H5); intros N H6; exists N; intros.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index ba17165061..9b5111ff93 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -99,7 +99,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
@@ -280,7 +280,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 28415ab618..092df1feb2 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1265,8 +1265,8 @@ Proof.
   apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
   apply INR_fact_neq_0.
   apply not_O_INR; discriminate.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   unfold Vn in |- *; rewrite Rmult_assoc; unfold Rdiv in |- *;
     rewrite (Rmult_comm (Un 0%nat)); rewrite (Rmult_comm (Un n)).
   repeat apply Rmult_le_compat_l.
@@ -1293,8 +1293,8 @@ Proof.
   apply le_INR; omega.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   intro; unfold Un in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
   apply pow_lt; assumption.
   apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;