Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

13 files changed, 2416 insertions, 833 deletions

diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 5060bc69..074f6ef7 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -7,20 +7,32 @@
 (************************************************************************)
 
 Require Import Mult.
+Require Import BinNat.
+Require Import Nnat.
 Require Export Ring.
 Set Implicit Arguments.
 
-Ltac isnatcst t :=
-  let t := eval hnf in t in
-  match t with
-    O => true
-  | S ?p => isnatcst p
-  | _ => false
-  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.
+
+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 :=
@@ -43,28 +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.
-
-
-Unboxed 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]).
+
diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v
index 0d0fe5a4..50902004 100644
--- a/contrib/setoid_ring/BinList.v
+++ b/contrib/setoid_ring/BinList.v
@@ -10,7 +10,7 @@ Set Implicit Arguments.
 Require Import BinPos.
 Require Export List.
 Require Export ListTactics.
-Open Scope positive_scope.
+Open Local Scope positive_scope.
 
 Section MakeBinList.
  Variable A : Type.
@@ -89,3 +89,5 @@ Section MakeBinList.
  Qed.
 
 End MakeBinList.
+
+
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index 786654ab..aad3a580 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -10,10 +10,10 @@ Require Import Ring_tac BinList Ring_polynom InitialRing.
 Require Export Field_theory.
 
  (* syntaxification *)
- Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv := 
+ Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := 
  let rec mkP t :=
     match Cst t with
-    | Ring_tac.NotConstant =>
+    | InitialRing.NotConstant =>
         match t with 
         | (radd ?t1 ?t2) => 
           let e1 := mkP t1 in
@@ -31,6 +31,13 @@ Require Export Field_theory.
           let e2 := mkP t2 in constr:(FEdiv e1 e2)
         | (rinv ?t1) =>
           let e1 := mkP t1 in constr:(FEinv e1)
+        | (rpow ?t1 ?n) =>
+          match CstPow n with
+          | InitialRing.NotConstant => 
+            let p := Find_at t fv in constr:(@FEX C p)
+          | ?c => let e1 := mkP t1 in constr:(FEpow e1 c)
+          end
+  
         | _ =>
           let p := Find_at t fv in constr:(@FEX C p)
         end
@@ -38,10 +45,10 @@ Require Export Field_theory.
     end
  in mkP t.
 
-Ltac FFV Cst add mul sub opp div inv t fv :=
+Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
  let rec TFV t fv :=
   match Cst t with
-  | Ring_tac.NotConstant =>
+  | InitialRing.NotConstant =>
       match t with
       | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
@@ -49,16 +56,24 @@ Ltac FFV Cst add mul sub opp div inv t fv :=
       | (opp ?t1) => TFV t1 fv
       | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (inv ?t1) => TFV t1 fv
+      | (pow ?t1 ?n) =>
+        match CstPow n with
+        | InitialRing.NotConstant => AddFvTail t fv
+        | _ => TFV t1 fv
+        end
       | _ => AddFvTail t fv
       end
   | _ => fv
   end 
  in TFV t fv.
 
-Ltac ParseFieldComponents lemma req :=
+Ltac ParseFieldComponents lemma :=
   match type of lemma with
-  | context [@FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi _ _] =>
-      (fun f => f add mul sub opp div inv C)
+  | context [
+     (*   PCond _ _ _  _ _ _ _  _ _  _ _ -> *)
+        (@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)
   | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
   end.
 
@@ -78,91 +93,244 @@ 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) *)
-Ltac Field_simplify lemma Cond_lemma req Cst_tac :=
-  let Make_tac :=
-    match type of lemma with
-    | forall l fe nfe,
-      _ = nfe -> 
-      PCond _ _ _ _ _ _ _ _ _ ->
-      req (FEeval ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv (C:=?C) ?phi l fe)
-        _ =>
-        let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
-        let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
-        let simpl_field H := protect_fv "field" in H in
-        fun f rl => f mkFV mkFE simpl_field lemma req rl;
-                    try (apply Cond_lemma; simpl_PCond req)
-    | _ => fail 1 "field anomaly: bad correctness lemma (rewr)"
-    end in
-  Make_tac ReflexiveRewriteTactic.
-(* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
-
-Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
-  field_lookup
-    (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl =>
-       pre(); Field_simplify field_simplify_ok cond_ok req cst_tac rl; post()).
-
-
-(* Generic form of field tactics *)
-Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
-  let R := match type of req with ?R -> _ => R end 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 x H)
-    | _ => (fun t => t ilemma)
-    end in
-  let Main r1 r2 :=
-    let fv := FV_tac r1 (@List.nil R) in
-    let fv := FV_tac r2 fv in
-    let fe1 := SYN_tac r1 fv in
-    let fe2 := SYN_tac r2 fv in
-    ParseExpr (lemma fv fe1 fe2)
-    ltac:(fun ilemma =>
-           apply ilemma || fail "field anomaly: failed in applying lemma";
-            [ SIMPL_tac | apply Cond_lemma; simpl_PCond req]) in
-  OnEquation req Main.
+Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl :=
+  let Main radd rmul rsub ropp rdiv rinv rpow C :=
+    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 fv := FV_hypo_tac mkFV req lH in
+    let simpl_field H := (protect_fv "field" in H;f H) in
+    let lemma_tac fv RW_tac :=
+      let rr_lemma := fresh "f_rw_lemma" in
+      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+      let vlpe := fresh "list_hyp" in
+      let vlmp := fresh "list_hyp_norm" in
+      let vlmp_eq := fresh "list_hyp_norm_eq" in
+      let prh := proofHyp_tac lH in
+      pose (vlpe := lpe);
+      match type of lemma with
+      | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] =>
+        compute_assertion vlmp_eq vlmp 
+            (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe);
+         (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq)
+          || fail "type error when build the rewriting lemma");
+         RW_tac rr_lemma;
+        try clear rr_lemma vlmp_eq vlmp vlpe
+      | _ => fail 1 "field_simplify anomaly: bad correctness lemma"
+      end in
+    ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl;
+    try (apply Cond_lemma; simpl_PCond req) in
+  ParseFieldComponents lemma Main.
+
+Ltac Field_simplify_gen f := 
+     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).
+
+Tactic Notation (at level 0) 
+  "field_simplify" constr_list(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) :=
+  match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end.
+
+Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=   
+   let G := getGoal in
+   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.
+
+Tactic Notation "field_simplify" "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=   
+   let G := getGoal in
+   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.
+
+(*
+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) :=
+  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) :=
+  let t := type of h in
+  field_lookup (Field_simplify_in h) [lH] rl [t].
+*)
+
+(** Generic tactic for solving equations *)
+
+Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH :=
+  let Main radd rmul rsub ropp rdiv rinv rpow C :=
+    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 x H)
+      | _ => (fun t => t ilemma)
+      end in
+    let Main_eq t1 t2 :=
+      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 vlpe := fresh "list_hyp" in
+      let fe1 := mkFE t1 fv in
+      let fe2 := mkFE t2 fv in
+      pose (vlpe := lpe);
+      let nlemma := fresh "field_lemma" in
+      (assert (nlemma := lemma n fv vlpe fe1 fe2 prh)
+       || fail "field anomaly:failed to build lemma"); 
+      ParseExpr nlemma
+         ltac:(fun ilemma =>
+                  apply ilemma 
+                  || fail "field anomaly: failed in applying lemma";
+                  [ Simpl_tac | apply Cond_lemma; simpl_PCond req]);
+      clear vlpe nlemma in
+    OnEquation req Main_eq in
+  ParseFieldComponents lemma Main.
 
 (* solve completely a field equation, leaving non-zero conditions to be
    proved (field) *)
-Ltac Field lemma Cond_lemma req Cst_tac :=
-  let Main radd rmul rsub ropp rdiv rinv C :=
-    let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
-    let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
-    let Simpl :=
-      vm_compute; reflexivity || fail "not a valid field equation" in
-    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
-  ParseFieldComponents lemma req Main.
 
+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 =>
+       pre(); 
+       Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req 
+         Ring_tac.ring_subst_niter lH;
+       try exact I;
+       post().
+ 
 Tactic Notation (at level 0) "field" :=
-  field_lookup
-    (fun req cst_tac field_ok _ _ cond_ok pre post rl =>
-       pre(); Field field_ok cond_ok req cst_tac; post()).
+  let G := getGoal in field_lookup FIELD [] [G].
+
+Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
+  let G := getGoal in field_lookup FIELD [lH] [G].
 
 (* transforms a field equation to an equivalent (simplified) ring equation,
    and leaves non-zero conditions to be proved (field_simplify_eq) *)
-Ltac Field_simplify_eq lemma Cond_lemma req Cst_tac :=
-  let Main radd rmul rsub ropp rdiv rinv C :=
-    let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
-    let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
-    let Simpl := (protect_fv "field") in
-    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
-  ParseFieldComponents lemma req Main.
-
-Tactic Notation (at level 0) "field_simplify_eq" :=
-  field_lookup
-    (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl =>
-       pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac;
-       post()).
 
+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 =>
+       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" :=  
+  let G := getGoal in field_lookup FIELD_SIMPL [] [G].
+
+Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=  
+  let G := getGoal in field_lookup FIELD_SIMPL [lH] [G].
+
+(* 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 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 :=
@@ -179,22 +347,59 @@ Ltac coerce_to_almost_field set ext f :=
   | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f)
   end.
 
-Ltac field_elements set ext fspec rk :=
+Ltac field_elements set ext fspec pspec sspec rk :=
   let afth := coerce_to_almost_field set ext fspec in
   let rspec := ring_of_field fspec in
-  ring_elements set ext rspec rk
-  ltac:(fun arth ext_r morph f => f afth ext_r morph).
-
-
-Ltac field_lemmas set ext inv_m fspec rk :=
-  field_elements set ext fspec rk
-  ltac:(fun afth ext_r morph =>
-    let field_ok := constr:(Field_correct set ext_r inv_m afth morph) in
-    let field_simpl_ok :=
-      constr:(Pphi_dev_div_ok set ext_r inv_m afth morph) in
-    let field_simpl_eq_ok :=
-      constr:(Field_simplify_eq_correct set ext_r inv_m afth morph) in
-    let cond1_ok := constr:(Pcond_simpl_gen set ext_r afth morph) in
-    let cond2_ok := constr:(Pcond_simpl_complete set ext_r afth morph) in
-    (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok
-                cond1_ok cond2_ok)).
+  ring_elements set ext rspec pspec sspec rk
+  ltac:(fun arth ext_r morph p_spec s_spec f => f afth ext_r morph p_spec s_spec).
+
+Ltac field_lemmas set ext inv_m fspec pspec sspec rk :=
+  let simpl_eq_lemma := 
+     match pspec with
+     | 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)
+     | Some _ => constr:(Field_rw_pow_correct)
+     end in
+  field_elements set ext fspec pspec sspec rk
+   ltac:(fun afth ext_r morph p_spec s_spec =>
+     match p_spec with
+     | mkhypo ?pp_spec => match s_spec with
+     | mkhypo ?ss_spec =>
+       let field_simpl_eq_ok :=
+         constr:(simpl_eq_lemma _ _ _  _ _ _  _ _ _ _ 
+                   set ext_r inv_m afth 
+                   _ _ _  _ _ _  _ _ _ morph 
+                   _ _ _ pp_spec _ ss_spec) in 
+       let field_simpl_ok :=
+         constr:(rw_lemma _ _ _  _ _ _  _ _ _ _
+                   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 := 
+         constr:(Pcond_simpl_gen set ext_r afth morph pp_spec) in
+       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 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 f810859c..ea8421cf 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -9,6 +9,7 @@
 Require Ring.
 Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List.
 Require Import ZArith_base.
+(*Require Import Omega.*)
 Set Implicit Arguments.
 
 Section MakeFieldPol.
@@ -29,7 +30,7 @@ Section MakeFieldPol.
  Variable Rsth : Setoid_Theory R 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;
@@ -94,9 +95,20 @@ Hint Resolve (ARadd_0_l  ARth) (ARadd_comm  ARth) (ARadd_assoc ARth)
              (ARopp_mul_l ARth) (ARopp_add  ARth) 
              (ARsub_def  ARth) .
 
-Notation NPEeval := (PEeval rO radd rmul rsub ropp phi).
-Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb).
-Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi).
+ (* Power coefficients *)
+ Variable Cpow : Set.
+ 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 ropp req phi get_sign.
+
+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 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).
@@ -105,7 +117,7 @@ Add Ring Rring : (ARth_SRth ARth).
 (* additional ring properties *)
 
 Lemma rsub_0_l : forall r, 0 - r == - r.
-intros; rewrite (ARsub_def ARth) in |- *; ring.
+intros; rewrite (ARsub_def ARth) in |- *;ring.
 Qed.
 
 Lemma rsub_0_r : forall r, r - 0 == r.
@@ -352,6 +364,20 @@ intros H1; apply f_equal with ( f := xO ); auto.
 intros H1 H2; case H1; injection H2; auto.
 Qed.
  
+Definition N_eq n1 n2 := 
+  match n1, n2 with
+  | N0, N0 => true
+  | Npos p1, Npos p2 => positive_eq p1 p2
+  | _, _ => false
+  end.
+
+Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2.
+Proof.
+  intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail).
+  assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2);
+     [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial].
+Qed.
+
 (* equality test *)
 Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
  match e1, e2 with
@@ -361,9 +387,25 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
   | 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_eq n3 n4 then PExpr_eq e3 e4 else false
   | _, _ => false
  end.
  
+Add Morphism (pow_pos rmul) : 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) : pow_N_morph.
+intros x y H [|p];simpl;auto. apply pow_morph;trivial.
+Qed.
+(*
+Lemma rpow_morph : forall x y n, x == y ->rpow x (Cp_phi n) == rpow y (Cp_phi n).
+Proof.
+  intros; repeat rewrite pow_th.(rpow_pow_N).
+  destruct n;simpl. apply eq_refl.
+  induction p;simpl;try rewrite IHp;try rewrite H; apply eq_refl.
+Qed.
+*)
 Theorem PExpr_eq_semi_correct:
  forall l e1 e2, PExpr_eq e1 e2 = true ->  NPEeval l e1 == NPEeval l e2.
 intros l e1; elim e1.
@@ -387,6 +429,10 @@ intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
 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;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4);
+intros;try discriminate.
+repeat rewrite  pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto.
 Qed.
 
 (* add *)
@@ -395,6 +441,7 @@ Definition NPEadd e1 e2 :=
     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.
 
@@ -403,32 +450,68 @@ Theorem NPEadd_correct:
 Proof.
 intros l e1 e2.
 destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
- try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
- try rewrite (morph0 CRmorph) in |- *; try ring.
-apply (morph_add CRmorph).
+ try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl;
+ try ring [(morph0 CRmorph)].
+ apply (morph_add CRmorph).
+Qed.
+
+Definition NPEpow x n :=
+  match n with
+  | N0 => PEc cI
+  | Npos p =>
+    if positive_eq 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).
+Proof.
+ destruct n;simpl.
+ rewrite pow_th.(rpow_pow_N);simpl;auto.
+ generalize (positive_eq_correct p xH).
+ destruct (positive_eq p 1);intros.
+ rewrite H;rewrite  pow_th.(rpow_pow_N). trivial.
+ clear H;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].
 Qed.
 
 (* mul *) 
-Definition NPEmul x y :=
+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
-  |  _, _ => PEmul x y
+  | PEpow e1 n1, PEpow e2 n2 =>
+      if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
+  | _, _ => PEmul x y
   end.
-             
+
+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.
+          
 Theorem NPEmul_correct : forall l e1 e2,
   NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2).
-intros l e1 e2.
-destruct e1; destruct e2; simpl in |- *; try reflexivity;
+induction e1;destruct e2; simpl in |- *;try reflexivity;
  repeat apply ceqb_rect;
- try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
- try rewrite (morph0 CRmorph) in |- *;
- try rewrite (morph1 CRmorph) in |- *;
- try ring.
-apply (morph_mul CRmorph).
+ try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity;
+ try ring [(morph0 CRmorph) (morph1 CRmorph)].
+ apply (morph_mul CRmorph).
+assert (H:=N_eq_correct n n0);destruct (N_eq n n0).
+rewrite NPEpow_correct. simpl.
+repeat rewrite pow_th.(rpow_pow_N).
+rewrite IHe1;rewrite <- H;destruct n;simpl;try ring.
+apply pow_pos_mul.
+simpl;auto.
 Qed.
 
 (* sub *)
@@ -437,6 +520,7 @@ Definition NPEsub e1 e2 :=
     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
+     (* Peut-on factoriser ici *)
   | _, _ => PEsub e1 e2
   end.
 
@@ -467,6 +551,7 @@ Fixpoint PExpr_simp (e : PExpr C) : PExpr C :=
   | 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
   | _ => e
  end.
  
@@ -489,6 +574,10 @@ 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.
 Qed.
 
 
@@ -508,8 +597,9 @@ Inductive FExpr : Type :=
  | FEmul: FExpr -> FExpr ->  FExpr
  | FEopp: FExpr ->  FExpr
  | FEinv: FExpr ->  FExpr
- | FEdiv: FExpr -> FExpr ->  FExpr .
-
+ | FEdiv: FExpr -> FExpr ->  FExpr
+ | FEpow: FExpr -> N -> FExpr .
+ 
 Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
   match pe with
   | FEc c     => phi c
@@ -520,6 +610,7 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
   | FEopp x   => - FEeval l x
   | FEinv x   => / FEeval l x
   | FEdiv x y => FEeval l x / FEeval l y
+  | FEpow x n => rpow (FEeval l x) (Cp_phi n)
   end.
 
 (* The result of the normalisation *)
@@ -538,8 +629,8 @@ 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 (PEeval rO radd rmul rsub ropp phi l e1) rO
-  | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO /\ PCond l l1
+  | e1 :: nil => ~ req (NPEeval l e1) rO
+  | e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1
   end.
 
 Theorem PCond_cons_inv_l :
@@ -584,66 +675,170 @@ Qed.
                                                                           
   ***************************************************************************)
 
-
-Fixpoint isIn (e1 e2: PExpr C) {struct e2}: option (PExpr C) :=
+Fixpoint isIn (e1:PExpr C)  (p1:positive)
+                      (e2:PExpr C)  (p2:positive) {struct e2}: option (N * PExpr C) :=
   match e2 with
   | PEmul e3 e4 =>
-       match isIn e1 e3 with
-         Some e5 => Some (NPEmul e5 e4)
-       | None => match isIn e1 e4 with
-                 | Some e5 => Some (NPEmul e3 e5)
-                 | None => None
-                 end
+       match isIn e1 p1 e3 p2 with
+       | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow 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)))
+          end
+       | None => 
+         match isIn e1 p1 e4 p2 with
+         | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5)
+         | None => None
+         end
        end
+  | PEpow e3 N0 => None 
+  | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2)
   | _ =>
-       if PExpr_eq e1 e2 then Some (PEc cI) else None
+     if  PExpr_eq e1 e2 then
+         match Zminus (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 
    end.
+ 
+ Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end.
+ Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end.
+
+ Notation pow_pos_plus :=  (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext) 
+                        ARth.(ARmul_comm) ARth.(ARmul_assoc)).
+
+ Lemma isIn_correct_aux : forall l e1 e2 p1 p2, 
+  match 
+      (if  PExpr_eq e1 e2 then
+         match Zminus (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
+   | 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
+  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.
+  case_eq ((p1 ?= p2)%positive Eq);intros;simpl. 
+  repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
+  rewrite (Pcompare_Eq_eq _ _ H0).  
+  rewrite H;[trivial | ring [ (morph1 CRmorph)]].
+  fold (NPEpow e2 (Npos (p2 - p1))).
+  rewrite NPEpow_correct;simpl.
+  repeat rewrite pow_th.(rpow_pow_N);simpl.
+  rewrite H;trivial. split. 2:refine (refl_equal _).
+  rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial. 
+  repeat rewrite pow_th.(rpow_pow_N);simpl.
+  rewrite H;trivial.
+   change (ZtoN
+     match (p1 ?= p1 - p2)%positive Eq with
+     | Eq => 0
+     | Lt => Zneg (p1 - p2 - p1)
+     | Gt => Zpos (p1 - (p1 - p2))
+     end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))).
+  replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
+  split.
+  repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
+  rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl.
+  ring [ (morph1 CRmorph)].
+ assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _). 
+ apply Zplus_gt_reg_l with (Zpos p2).
+ rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
+ apply Zplus_gt_compat_r. refine (refl_equal _).
+ simpl;rewrite H0;trivial.
+Qed.
+
+Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
+induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_plus;simpl.
+ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto.
+Qed.
+
 
-Theorem isIn_correct: forall l e1 e2,
-  match isIn e1 e2 with 
-    (Some e3) => NPEeval l e2 == NPEeval l (NPEmul e1 e3)
-  |  _ => True
+Theorem isIn_correct: forall l 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
+   |  _ => True
   end.
 Proof.
-intros l e1 e2; elim e2; simpl; auto.
-  intros c;
-   generalize (PExpr_eq_semi_correct l e1 (PEc c));
-   case (PExpr_eq e1 (PEc c)); simpl; auto; intros H.
-   rewrite NPEmul_correct; simpl; auto.
-   rewrite H; auto; simpl. 
-   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
-  intros p;
-   generalize (PExpr_eq_semi_correct l e1 (PEX C p));
-   case (PExpr_eq e1 (PEX C p)); simpl; auto; intros H.
-   rewrite NPEmul_correct; simpl; auto.
-   rewrite H; auto; simpl. 
-   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
- intros p Hrec p1 Hrec1.
-   generalize (PExpr_eq_semi_correct l e1 (PEadd p p1));
-   case (PExpr_eq e1 (PEadd p p1)); simpl; auto; intros H.
-   rewrite NPEmul_correct; simpl; auto.
-   rewrite H; auto; simpl. 
-   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
- intros p Hrec p1 Hrec1.
-   generalize (PExpr_eq_semi_correct l e1 (PEsub p p1));
-   case (PExpr_eq e1 (PEsub p p1)); simpl; auto; intros H.
-   rewrite NPEmul_correct; simpl; auto.
-   rewrite H; auto; simpl. 
-   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
- intros p; case (isIn e1 p).
-   intros p2 Hrec p1 Hrec1.
-   rewrite Hrec; auto; simpl. 
-   repeat (rewrite NPEmul_correct; simpl; auto).
-   intros _ p1; case (isIn e1 p1); auto.
-   intros p2 H; rewrite H.
-   repeat (rewrite NPEmul_correct; simpl; auto).
-   ring.
-  intros p;
-   generalize (PExpr_eq_semi_correct l e1 (PEopp p));
-   case (PExpr_eq e1 (PEopp p)); simpl; auto; intros H.
-   rewrite NPEmul_correct; simpl; auto.
-   rewrite H; auto; simpl. 
-   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
+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).
+    unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;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_plus. rewrite Pplus_minus.
+   split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
+   repeat rewrite pow_th.(rpow_pow_N);simpl. 
+   intros (H1,H2) (H3,H4).
+   unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
+   rewrite H2 in H1;simpl in H1.
+   assert (Zpos p1 > Zpos p6)%Z.
+     apply Zgt_trans with (Zpos p4). exact H4. exact H2.
+  unfold Zgt in H;simpl in H;rewrite H.
+  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_plus.
+  replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. 
+ rewrite NPEmul_correct. simpl;ring.
+  assert 
+     (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
+ change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
+ rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)).
+ simpl. rewrite Pcompare_refl. reflexivity.
+ unfold Zminus, Zopp in H0. simpl in H0.
+  rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
+ simpl. repeat rewrite pow_th.(rpow_pow_N). 
+ intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3.
+ 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.
+   unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1.
+   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.
 Qed.
 
 Record rsplit : Type := mk_rsplit {
@@ -652,90 +847,94 @@ Record rsplit : Type := mk_rsplit {
    rsplit_right : PExpr C}.
 
 (* Stupid name clash *)
-Let left := rsplit_left.
-Let right := rsplit_right.
-Let common := rsplit_common.
+Notation left := rsplit_left.
+Notation right := rsplit_right.
+Notation common := rsplit_common.
 
-Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit :=
+Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit :=
   match e1 with
   | PEmul e3 e4 =>
-      let r1 := split e3 e2 in
-      let r2 := split e4 (right r1) in
+      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 (Pmult p3 p) e2      
   | _ => 
-       match isIn e1 e2 with
-         Some e3 => mk_rsplit (PEc cI) e1 e3
-       | None => mk_rsplit e1 (PEc cI) 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
        end
   end. 
 
-Theorem split_correct: forall l e1 e2,
-  NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2))
-                                   (common (split e1 e2)))
-/\
-  NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
-                                   (common (split e1 e2))).
+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 l e1; elim e1; simpl; auto.
-  intros c e2; generalize (isIn_correct l (PEc c) e2);
-    case (isIn (PEc c) e2); auto; intros p;
-    [intros Hp1; rewrite Hp1 | idtac];
-    simpl left; simpl common;  simpl right; auto;
-    repeat rewrite NPEmul_correct; simpl; split; 
-    try rewrite  (morph1 CRmorph); ring.
-  intros p e2; generalize (isIn_correct l (PEX C p) e2);
-    case (isIn (PEX C p) e2); auto; intros p1;
-    [intros Hp1; rewrite Hp1 | idtac];
-    simpl left; simpl common;  simpl right; auto;
-    repeat rewrite NPEmul_correct; simpl; split; 
-    try rewrite  (morph1 CRmorph); ring.
-  intros p1 _ p2 _ e2; generalize (isIn_correct l (PEadd p1 p2) e2);
-    case (isIn (PEadd p1 p2) e2); auto; intros p;
-    [intros Hp1; rewrite Hp1 | idtac];
-    simpl left; simpl common;  simpl right; auto;
-    repeat rewrite NPEmul_correct; simpl; split; 
-    try rewrite  (morph1 CRmorph); ring.
-  intros p1 _ p2 _ e2; generalize (isIn_correct l (PEsub p1 p2) e2);
-    case (isIn (PEsub p1 p2) e2); auto; intros p;
-    [intros Hp1; rewrite Hp1 | idtac];
-    simpl left; simpl common;  simpl right; auto;
-    repeat rewrite NPEmul_correct; simpl; split; 
-    try rewrite  (morph1 CRmorph); ring.
-  intros p1 Hp1 p2 Hp2 e2.
-    repeat rewrite NPEmul_correct; simpl; split.
-    case (Hp1 e2); case (Hp2 (right (split p1 e2))).
-    intros tmp1 _ tmp2 _; rewrite tmp1; rewrite tmp2.
-    repeat rewrite NPEmul_correct; simpl.
-    ring.
-    case (Hp1 e2); case (Hp2 (right (split p1 e2))).
-    intros _ tmp1 _ tmp2; rewrite tmp2;
-    repeat rewrite NPEmul_correct; simpl.
-    rewrite tmp1.
-    repeat rewrite NPEmul_correct; simpl.
-    ring.
-  intros p _ e2; generalize (isIn_correct l (PEopp p) e2);
-    case (isIn (PEopp p) e2); auto; intros p1;
-    [intros Hp1; rewrite Hp1 | idtac];
-    simpl left; simpl common;  simpl right; auto;
-    repeat rewrite NPEmul_correct; simpl; split; 
-    try rewrite  (morph1 CRmorph); ring.
+ intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH).
+ destruct (isIn e1 p e2 1). destruct p0.
+ 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). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H.
+  simpl in H;split;try ring [H].
+  rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
+  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].
+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))).
 Proof.
-intros l e1 e2; case (split_correct l e1 e2); auto.
+intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl.
+rewrite pow_th.(rpow_pow_N);simpl;auto.
 Qed.
 
 Theorem split_correct_r: forall l e1 e2,
   NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
                                    (common (split e1 e2))).
 Proof.
-intros l e1 e2; case (split_correct l e1 e2); auto.
+intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto.
 Qed.
 
 Fixpoint Fnorm (e : FExpr) : linear := 
@@ -777,6 +976,9 @@ Fixpoint Fnorm (e : FExpr) : linear :=
       mk_linear (NPEmul (num x) (denum y))
         (NPEmul (denum x) (num y))
         (num y :: condition x ++ condition y)
+  | FEpow e1 n =>
+      let x := Fnorm e1 in
+      mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x)
   end.
 
 
@@ -789,6 +991,17 @@ 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.
+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). rewrite H1. rewrite Hp;ring. ring.
+  reflexivity. 
+  intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
+  rewrite Hp;ring. reflexivity. trivial.
+Qed.
+ 
 Theorem Pcond_Fnorm:
  forall l e,
  PCond l (condition (Fnorm e)) ->  ~ NPEeval l (denum (Fnorm e)) == 0.
@@ -849,6 +1062,11 @@ intros l e; elim e.
     specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
     apply PCond_app_inv_l with (1 := Hcond1).
    apply PCond_cons_inv_l with (1:=Hcond).
+ 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.
 
@@ -928,6 +1146,23 @@ rewrite (He1 HH1); rewrite (He2 HH2).
 repeat rewrite NPEmul_correct;simpl.
 apply rdiv7; auto.
 apply PCond_cons_inv_l with ( 1 := HH ).
+
+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).
+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.
+rewrite IHp;reflexivity.
+reflexivity.
 Qed.
 
 Theorem Fnorm_crossproduct:
@@ -951,17 +1186,22 @@ rewrite Fnorm_FEeval_PEeval in |- *.
 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).
 
 Theorem Fnorm_correct:
- forall l fe,
- Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true ->
- PCond l (condition (Fnorm fe)) ->  FEeval l fe == 0.
-intros l fe H H1;
+ 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.
-apply (ring_correct Rsth Reqe ARth CRmorph); auto.
-simpl; apply (morph0 CRmorph); auto.
+rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_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.
 Qed.
 
 (* simplify a field expression into a fraction *)
@@ -969,31 +1209,50 @@ Qed.
 Definition display_linear l num den :=
   NPphi_dev l num / NPphi_dev l den.
 
-Theorem Pphi_dev_div_ok:
- forall l fe nfe,
- Fnorm fe = nfe ->
- PCond l (condition nfe) ->
- FEeval l fe == display_linear l (Nnorm (num nfe)) (Nnorm (denum nfe)).
+Definition display_pow_linear l num den :=
+  NPphi_pow l num / NPphi_pow l den.
+
+Theorem Field_rw_correct :
+ forall 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)).
 Proof.
-  intros l fe nfe eq_nfe H; subst nfe.
+  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;
-  apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity.
+  eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto.
+Qed.
+
+Theorem Field_rw_pow_correct :
+ forall 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)).
+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.
 Qed.
 
-(* solving a field equation *)
 Theorem Field_correct :
- forall l fe1 fe2,
+ 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 ->
- Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2)))
-          (Nnorm (PEmul (num nfe2) (denum nfe1))) = true ->
+ Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2)))
+          (Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros l fe1 fe2 nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2.
+intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp.
 apply Fnorm_crossproduct; trivial.
-apply (ring_correct Rsth Reqe ARth CRmorph); trivial.
+eapply (ring_correct Rsth Reqe ARth CRmorph); eauto.
 Qed.
 
 (* simplify a field equation : generate the crossproduct and simplify
@@ -1002,47 +1261,204 @@ Theorem Field_simplify_eq_old_correct :
  forall l fe1 fe2 nfe1 nfe2,
  Fnorm fe1 = nfe1 ->
  Fnorm fe2 = nfe2 ->
- NPphi_dev l (Nnorm (PEmul (num nfe1) (denum nfe2))) ==
- NPphi_dev l (Nnorm (PEmul (num nfe2) (denum nfe1))) ->
+ 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.
-rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *.
-rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *.
+match goal with 
+ [ |- NPEeval l ?x == NPEeval l ?y] =>
+    rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec
+       O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x)));
+    rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec
+       O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y)))
+ end.
 trivial.
 Qed.
 
 Theorem Field_simplify_eq_correct :
- forall l fe1 fe2,
+ 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 -> 
- NPphi_dev l (Nnorm (PEmul (num nfe1) (right den))) ==
- NPphi_dev l (Nnorm (PEmul (num nfe2) (left den))) ->
+ NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
+ NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros l fe1 fe2 nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
-  subst nfe1 nfe2 den.
+intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond;
+  subst nfe1 nfe2 den lmp.
 apply Fnorm_crossproduct; trivial.
 simpl in |- *.
-elim (split_correct l (denum (Fnorm fe1)) (denum (Fnorm fe2))); intros.
-rewrite H in |- *.
-rewrite H0 in |- *.
-clear H H0.
+rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
+rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
 rewrite NPEmul_correct in |- *.
 rewrite NPEmul_correct in |- *.
 simpl in |- *.
 repeat rewrite (ARmul_assoc ARth) in |- *.
-rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod.
-rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod.
+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 get_sign_spec n lpe l 
+        Hlpe (refl_equal (Nmk_monpol_list lpe))
+        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+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 get_sign_spec n lpe l 
+        Hlpe (refl_equal (Nmk_monpol_list lpe))
+        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
 simpl in Hcrossprod.
 rewrite Hcrossprod in |- *.
 reflexivity.
 Qed.
 
+Theorem Field_simplify_eq_pow_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 -> 
+ NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) ==
+ NPphi_pow l (Nnorm n lmp (PEmul (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.
+simpl in |- *.
+rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
+rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *.
+rewrite NPEmul_correct in |- *.
+rewrite NPEmul_correct in |- *.
+simpl in |- *.
+repeat rewrite (ARmul_assoc ARth) in |- *.
+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 get_sign_spec n lpe l 
+        Hlpe (refl_equal (Nmk_monpol_list lpe))
+        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+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 get_sign_spec n lpe l 
+        Hlpe (refl_equal (Nmk_monpol_list lpe))
+        x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod.
+simpl in Hcrossprod.
+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).
@@ -1100,7 +1516,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
  match l with
    nil       => cons e nil
  | cons a l1 =>
-     if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1)
+     if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l else cons a (Fcons0 e l1)
  end.
  
 Theorem PFcons0_fcons_inv:
@@ -1108,8 +1524,8 @@ Theorem PFcons0_fcons_inv:
 intros l a l1; elim l1; simpl Fcons0; auto.
 simpl; auto.
 intros a0 l0.
-generalize (ring_correct Rsth Reqe ARth CRmorph l a a0);
-  case (Peq ceqb (Nnorm a) (Nnorm a0)).
+generalize (ring_correct Rsth Reqe ARth CRmorph pow_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.
@@ -1125,6 +1541,7 @@ Qed.
 Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
  match e with
    PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l)
+ | PEpow e1 _ => Fcons00 e1 l
  | _ => Fcons0 e l
  end.
 
@@ -1137,9 +1554,12 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
    case (H0 _ H3); intros H4 H5; split; auto.
    simpl in |- *.
    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.
 Qed.
 
-
 Definition Pcond_simpl_gen := 
   fcons_correct _ PFcons00_fcons_inv.
 
@@ -1167,6 +1587,7 @@ 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)
+ | 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
  | _ => Fcons0 e l
@@ -1196,6 +1617,9 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
     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.
 Qed.
 
 Definition Fcons2 e l := Fcons1 (PExpr_simp e) l.
@@ -1214,30 +1638,6 @@ Definition Pcond_simpl_complete :=
 
 End Fcons_simpl.
 
-Let Mpc := MPcond_map cO cI cadd cmul csub copp ceqb.
-Let Mp := MPcond_dev rO rI radd rmul req cO cI ceqb phi.
-Let Subst := PNSubstL cO cI cadd cmul ceqb.
-
-(* simplification + rewriting *)
-Theorem Field_subst_correct :
-forall l ul fe m n,
- PCond l (Fapp Fcons00 (condition (Fnorm fe)) nil) ->
- Mp (Mpc ul) l ->
- Peq ceqb (Subst (Nnorm (num (Fnorm fe))) (Mpc ul) m n) (Pc cO) = true ->
- FEeval l fe == 0.
-intros l ul fe m n H H1 H2.
-assert (H3 := (Pcond_simpl_gen _ _ H)).
-apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe 
-                           (Pcond_simpl_gen _ _ H)).
-apply rdiv8; auto.
-rewrite (PNSubstL_dev_ok Rsth Reqe ARth CRmorph m n
-              _ (num (Fnorm fe)) l H1).
-rewrite <-(Ring_polynom.Pphi_Pphi_dev Rsth Reqe ARth CRmorph).
-rewrite (fun x => Peq_ok Rsth Reqe CRmorph x (Pc cO)); auto.
-simpl; apply (morph0 CRmorph); auto.
-Qed.
-
-
 End AlmostField.
 
 Section FieldAndSemiField.
@@ -1457,4 +1857,3 @@ Qed.
 End Field.
 
 End Complete.
-
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 7df68cc0..bbdcd443 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -7,16 +7,21 @@
 (************************************************************************)
 
 Require Import ZArith_base.
+Require Import Zpow_def.
 Require Import BinInt.
 Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_theory.
-Require Import Ring_tac.
 Require Import Ring_polynom.
+
 Set Implicit Arguments.
 
 Import RingSyntax.
 
+
+(* An object to return when an expression is not recognized as a constant *)
+Definition NotConstant := false.
+
 (** Z is a ring and a setoid*)
 
 Lemma Zsth : Setoid_Theory Z (@eq Z).
@@ -88,6 +93,21 @@ Section ZMORPHISM.
   | Zneg p => -(gen_phiPOS p)
   end.
  Notation "[ x ]" := (gen_phiZ x).   
+
+ Definition get_signZ z :=
+  match z with
+  | Zneg p => Some (Zpos p) 
+  | _ => None
+  end.
+
+ Lemma get_signZ_th : sign_theory ropp req gen_phiZ get_signZ.
+ Proof.
+  constructor.
+  destruct c;intros;try discriminate.
+  injection H;clear H;intros H1;subst c'.
+  simpl;rrefl.
+ Qed.
+
  
  Section ALMOST_RING.
  Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
@@ -346,7 +366,8 @@ Section NMORPHISM.
 End NMORPHISM.
 
  (* syntaxification of constants in an abstract ring:
-    the inverse of gen_phiPOS *)
+    the inverse of gen_phiPOS 
+    Why we do not reconnize only rI ?????? *)
  Ltac inv_gen_phi_pos rI add mul t :=
    let rec inv_cst t :=
    match t with
@@ -396,65 +417,8 @@ End NMORPHISM.
      end
    end.
 
-(* coefs = Z (abstract ring) *)
-Module Zpol.
-
-Definition ring_gen_correct
-  R rO rI radd rmul rsub ropp req rSet req_th Rth :=
-  @ring_correct R rO rI radd rmul rsub ropp req rSet req_th
-                (Rth_ARth rSet req_th Rth)
-                Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
-                (@gen_phiZ R rO rI radd rmul ropp)
-                (gen_phiZ_morph rSet req_th Rth).
-
-Definition ring_rw_gen_correct
-  R rO rI radd rmul rsub ropp req rSet req_th Rth :=
-  @Pphi_dev_ok   R rO rI radd rmul rsub ropp req rSet req_th
-                 (Rth_ARth rSet req_th Rth)
-                 Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
-                 (@gen_phiZ R rO rI radd rmul ropp)
-                 (gen_phiZ_morph rSet req_th Rth).
-
-Definition ring_gen_eq_correct R rO rI radd rmul rsub ropp Rth :=
-  @ring_gen_correct
-     R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth.
-
-Definition ring_rw_gen_eq_correct R rO rI radd rmul rsub ropp Rth :=
-  @ring_rw_gen_correct
-     R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth.
-
-End Zpol.
-
-(* coefs = N (abstract semi-ring) *)
-Module Npol.
-
-Definition ring_gen_correct
-  R rO rI radd rmul req rSet req_th SRth :=
-  @ring_correct R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet
-                (SReqe_Reqe req_th)
-                (SRth_ARth rSet SRth)
-                N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool
-                (@gen_phiN R rO rI radd rmul)
-                (gen_phiN_morph rSet req_th SRth).
-
-Definition ring_rw_gen_correct
-  R rO rI radd rmul req rSet req_th SRth :=
-  @Pphi_dev_ok   R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet
-                 (SReqe_Reqe req_th)
-                 (SRth_ARth rSet SRth)
-                 N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool
-                 (@gen_phiN R rO rI radd rmul)
-                 (gen_phiN_morph rSet req_th SRth).
-
-Definition ring_gen_eq_correct R rO rI radd rmul SRth :=
-  @ring_gen_correct
-     R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth.
-
-Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth :=
-  @ring_rw_gen_correct
-     R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth.
-
-End Npol.
+(* A simpl tactic reconninzing nothing *)
+ Ltac inv_morph_nothing t := constr:(NotConstant).
 
 
 Ltac coerce_to_almost_ring set ext rspec :=
@@ -481,7 +445,47 @@ Ltac abstract_ring_morphism set ext rspec :=
   | _ => fail 1 "bad ring structure"
   end.
 
-Ltac ring_elements set ext rspec rk :=
+Record hypo : Type := mkhypo {
+   hypo_type : Type;
+   hypo_proof : hypo_type
+ }.
+
+Ltac gen_ring_pow set arth pspec :=
+ match pspec with
+ | None =>
+   match type of arth with
+   | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
+     constr:(mkhypo (@pow_N_th R rI rmul req set))
+   | _ => fail 1 "gen_ring_pow"
+   end
+ | Some ?t => constr:(t)
+ end.
+
+Ltac default_sign_spec morph :=
+ match type of morph with
+ | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req 
+               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
+      constr:(mkhypo (@get_sign_None_th R ropp req C phi))
+ | _ => fail 1 "ring anomaly : default_sign_spec" 
+ end.
+
+Ltac gen_ring_sign set rspec morph sspec rk :=
+ match sspec with
+ | None =>
+   match rk with
+   | Abstract =>
+     match type of rspec with
+     | @ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
+       constr:(mkhypo (@get_signZ_th R rO rI radd rmul ropp req set))
+     | _ => default_sign_spec morph 
+     end
+   | _ => default_sign_spec morph 
+   end
+ | 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
   let morph :=
@@ -493,19 +497,85 @@ Ltac ring_elements set ext rspec 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
-  fun f => f arth ext_r morph.
+  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
+    | None => constr:(ring_rw_correct) 
+    | Some _ => constr:(ring_rw_pow_correct)
+    end in
+  ring_elements set ext rspec pspec sspec rk
+    ltac:(fun arth ext_r morph p_spec s_spec =>
+        match p_spec with
+        | mkhypo ?pp_spec =>
+        match s_spec with
+        | mkhypo ?ps_spec =>
+          let lemma1 := 
+            constr:(ring_correct set ext_r arth morph pp_spec) in
+          let lemma2 := 
+            constr:(gen_lemma2 _  _ _  _ _ _  _  _ set ext_r arth 
+                           _  _ _  _ _ _  _  _  _ morph 
+                           _ _ _ pp_spec
+                           _ ps_spec) in 
+          fun f => f arth ext_r morph lemma1 lemma2
+        | _ => fail 2 "bad sign specification"
+       end
+       | _ => fail 1 "bad power specification" 
+       end).
+ 
+(* Tactic for constant *)
+Ltac isnatcst t :=
+  match t with
+    O => true
+  | S ?p => isnatcst p
+  | _ => false
+  end.
+
+Ltac isPcst t :=
+  match t with
+  | xI ?p => isPcst p
+  | xO ?p => isPcst p
+  | xH => constr:true
+  (* nat -> positive *)
+  | P_of_succ_nat ?n => isnatcst n 
+  | _ => false
+  end.
+
+Ltac isNcst t :=
+  match t with
+    N0 => constr:true
+  | Npos ?p => isPcst p
+  | _ => constr:false
+  end.
+
+Ltac isZcst t :=
+  match t with
+    Z0 => true
+  | Zpos ?p => isPcst p
+  | Zneg ?p => isPcst p
+  (* injection nat -> Z *)
+  | Z_of_nat ?n => isnatcst n
+  (* injection N -> Z *)
+  | Z_of_N ?n => isNcst n
+  (* *)
+  | _ => false
+  end.
+
+
 
-Ltac ring_lemmas set ext rspec rk :=
-  ring_elements set ext rspec rk
-    ltac:(fun arth ext_r morph =>
-      let lemma1 := constr:(ring_correct set ext_r arth morph) in
-      let lemma2 := constr:(Pphi_dev_ok set ext_r arth morph) in
-      fun f => f arth ext_r morph lemma1 lemma2).
 
 
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index 33e3cb4e..ae067a8a 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -12,16 +12,6 @@ Import InitialRing.
 
 Set Implicit Arguments.
 
-Ltac isNcst t :=
-  let t := eval hnf in t in
-  match t with
-    N0 => constr:true
-  | Npos ?p => isNcst p
-  | xI ?p => isNcst p
-  | xO ?p => isNcst p
-  | xH => constr:true
-  | _ => constr:false
-  end.
 Ltac Ncst t :=
   match isNcst t with
     true => t
diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index 13896123..d0512dff 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -1,6 +1,9 @@
-Require Import Raxioms.
-Require Import Rdefinitions.
+Require Import Nnat.
+Require Import ArithRing. 
 Require Export Ring Field.
+Require Import Rdefinitions.
+Require Import Rpow_def.
+Require Import Raxioms.
 
 Open Local Scope R_scope.
 
@@ -102,4 +105,29 @@ Lemma Zeq_bool_complete : forall x y,
   Zeq_bool x y = true.
 Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
 
-Add Field RField : Rfield (infinite Zeq_bool_complete).
+Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x  (n + m) = pow x n * pow x m.
+Proof.
+  intros x n; elim n; simpl in |- *; auto with real.
+  intros n0 H' m; rewrite H'; auto with real.
+Qed.
+
+Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R))  nat_of_N pow.
+Proof.
+ constructor. destruct n. reflexivity.
+ simpl. induction p;simpl. 
+ rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. reflexivity.
+ unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial.
+ rewrite Rmult_comm;apply Rmult_1_l.
+Qed.
+
+Ltac Rpow_tac t := 
+  match isnatcst t with
+  | false => constr:(InitialRing.NotConstant)
+  | _ => constr:(N_of_nat t)
+  end. 
+
+Add Field RField : Rfield  
+   (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
+
+
+ 
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index 167e026f..1a4e1cc7 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -9,6 +9,7 @@
 Require Import Bool.
 Require Export Ring_theory.
 Require Export Ring_base.
+Require Export InitialRing.
 Require Export Ring_tac.
 
 Lemma BoolTheory :
@@ -25,7 +26,7 @@ reflexivity.
 destruct x; reflexivity.
 Qed.
 
-Unboxed Definition bool_eq (b1 b2:bool) :=
+Definition bool_eq (b1 b2:bool) :=
   if b1 then b2 else negb b2.
 
 Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2.
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index 7317ab21..b79f2fe2 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -1,5 +1,5 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(*  V      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
@@ -10,9 +10,11 @@ Set Implicit Arguments.
 Require Import Setoid.
 Require Import BinList.
 Require Import BinPos.
+Require Import BinNat.
 Require Import BinInt.
 Require Export Ring_theory.
 
+Open Local Scope positive_scope.
 Import RingSyntax.
 
 Section MakeRingPol.
@@ -35,6 +37,12 @@ Section MakeRingPol.
  Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
                                 cO cI cadd cmul csub copp ceqb phi.
 
+  (* Power coefficients *)
+ Variable Cpow : Set.
+ Variable Cp_phi : N -> Cpow.
+ Variable rpow : R -> Cpow -> R. 
+ Variable pow_th : power_theory rI rmul req Cp_phi rpow.
+
 
  (* R notations *)
  Notation "0" := rO. Notation "1" := rI.
@@ -113,12 +121,23 @@ Section MakeRingPol.
   | _ => Pinj j P
   end.
 
+ Definition mkPinj_pred j P:=
+  match j with
+  | xH => P
+  | xO j => Pinj (Pdouble_minus_one j) P
+  | xI j => Pinj (xO j) P
+  end.
+
  Definition mkPX P i Q := 
   match P with
   | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q
   | Pinj _ _ => PX P i Q
   | PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q
   end.
+
+ Definition mkXi i := PX P1 i P0.
+
+ Definition mkX := mkXi 1.
  
  (** Opposite of addition *)
  
@@ -305,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'
@@ -319,10 +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 **)
      
@@ -331,29 +388,29 @@ Section MakeRingPol.
   | zmon: positive -> Mon -> Mon 
   | vmon: positive -> Mon -> Mon.
 
- Fixpoint pow (x:R) (i:positive) {struct i}: R :=
-  match i with
-  | xH => x
-  | xO i => let p := pow x i in p * p
-  | xI i => let p := pow x i in x * p * p
-  end.
-
  Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R :=
   match M with
      mon0 => rI
   | zmon j M1  => Mphi (jump j l) M1
   | vmon i M1 =>
      let x := hd 0 l in
-     let xi := pow x i in
+     let xi := pow_pos rmul x i in
     (Mphi (tail l) M1) * xi 
   end.
 
- Definition zmon_pred j M :=
-   match j with xH => M | _ => zmon (Ppred j) M end.
-
  Definition mkZmon j M :=
    match M with mon0 => mon0 | _ => zmon j M end.
 
+ Definition zmon_pred j M :=
+   match j with xH => M | _ => mkZmon (Ppred j) M end.
+
+ Definition mkVmon i M :=
+   match M with 
+   | mon0 => vmon i mon0 
+   | zmon j m => vmon i (zmon_pred j m)
+   | vmon i' m => vmon (i+i') m
+   end.
+
  Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
    match P, M with
         _, mon0 => (Pc cO, P)
@@ -434,7 +491,7 @@ Section MakeRingPol.
   | Pinj j Q => Pphi (jump j l) Q
   | PX P i Q => 
      let x := hd 0 l in
-     let xi := pow x i in
+     let xi := pow_pos rmul x i in
     (Pphi l P) * xi + (Pphi (tail l) Q)      
   end.
 
@@ -469,26 +526,6 @@ Section MakeRingPol.
   rewrite Psucc_o_double_minus_one_eq_xO;trivial.
   simpl;trivial.
  Qed.
-
- Lemma pow_Psucc : forall x j, pow x (Psucc j) == x * pow x j.
- Proof.
-  induction j;simpl;rsimpl.
-  rewrite IHj;rsimpl;mul_push x;rrefl.
- Qed.
-
- Lemma pow_Pplus : forall x i j, pow x (i + j) == pow x i * pow x j.
- Proof.
-  intro x;induction i;intros.
-  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat rewrite IHi.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc.
-  simpl;rsimpl.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat rewrite IHi;rsimpl.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc;
-   simpl;rsimpl.
- Qed.
   
  Lemma Peq_ok : forall P P', 
     (P ?== P') = true -> forall l, P@l == P'@ l.
@@ -523,8 +560,11 @@ Section MakeRingPol.
   rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl.
  Qed.
 
+ Let pow_pos_Pplus := 
+    pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
+
  Lemma mkPX_ok : forall l P i Q, 
-  (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tail l).
+  (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l).
  Proof.
   intros l P i Q;unfold mkPX.
   destruct P;try (simpl;rrefl).
@@ -533,7 +573,7 @@ Section MakeRingPol.
   rewrite mkPinj_ok;rsimpl;simpl;rrefl.
   assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl.
   rewrite (H (refl_equal true));trivial.
-  rewrite Pphi0;rewrite pow_Pplus;rsimpl.
+  rewrite Pphi0.  rewrite pow_pos_Pplus;rsimpl.
  Qed.
 
  Ltac Esimpl :=
@@ -622,19 +662,19 @@ Section MakeRingPol.
   Esimpl2;add_push [c];rrefl.
   destruct p0;simpl;Esimpl2.
   rewrite IHP'2;simpl.
-  rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl.
+  rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
   rewrite IHP'2;simpl.
-  rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl.
+  rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
   rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl.
   assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
   rewrite IHP'1;rewrite IHP'2;rsimpl.
   add_push (P3 @ (tail l));rewrite H;rrefl.
   rewrite IHP'1;rewrite IHP'2;simpl;Esimpl.
   rewrite H;rewrite Pplus_comm.
-  rewrite pow_Pplus;rsimpl.
+  rewrite pow_pos_Pplus;rsimpl.
   add_push (P3 @ (tail l));rrefl.
   assert (forall P k l, 
-           (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k).
+           (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k).
    induction P;simpl;intros;try apply (ARadd_comm ARth).
    destruct p2;simpl;try apply (ARadd_comm ARth).
    rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth).
@@ -642,15 +682,15 @@ Section MakeRingPol.
     rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl.
     rewrite IHP'1;simpl;Esimpl.
     rewrite H1;rewrite Pplus_comm.
-    rewrite pow_Pplus;simpl;Esimpl.
+    rewrite pow_pos_Pplus;simpl;Esimpl.
     add_push (P5 @ (tail l0));rrefl.
     rewrite IHP1;rewrite H1;rewrite Pplus_comm.
-    rewrite pow_Pplus;simpl;rsimpl.
+    rewrite pow_pos_Pplus;simpl;rsimpl.
     add_push (P5 @ (tail l0));rrefl.
   rewrite H0;rsimpl.
   add_push (P3 @ (tail l)).
   rewrite H;rewrite Pplus_comm.
-  rewrite IHP'2;rewrite pow_Pplus;rsimpl.
+  rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl.
   add_push (P3 @ (tail l));rrefl.
  Qed.
 
@@ -674,20 +714,20 @@ Section MakeRingPol.
   destruct P;simpl. 
   repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl.
   destruct p0;simpl;Esimpl2.
-  rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));trivial.
+  rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial.
   add_push (P @ (jump p0 (jump p0 (tail l))));rrefl.
   rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl.
-  add_push (- (P'1 @ l * pow (hd 0 l) p));rrefl.
+  add_push (- (P'1 @ l * pow_pos  rmul (hd 0 l) p));rrefl.
   rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl.
   assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
   rewrite IHP'1; rewrite IHP'2;rsimpl.
   add_push (P3 @ (tail l));rewrite H;rrefl.
    rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl.
   rewrite H;rewrite Pplus_comm.
-  rewrite pow_Pplus;rsimpl.
+  rewrite pow_pos_Pplus;rsimpl.
   add_push (P3 @ (tail l));rrefl.
   assert (forall P k l, 
-           (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k).
+           (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k).
    induction P;simpl;intros.
    rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial.
    destruct p2;simpl;rewrite Popp_ok;rsimpl.
@@ -697,17 +737,44 @@ Section MakeRingPol.
     assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl.
     rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl.
     rewrite IHP'1;rewrite H1;rewrite Pplus_comm.
-    rewrite pow_Pplus;simpl;Esimpl.
+    rewrite pow_pos_Pplus;simpl;Esimpl.
     add_push (P5 @ (tail l0));rrefl.
     rewrite IHP1;rewrite H1;rewrite Pplus_comm.
-    rewrite pow_Pplus;simpl;rsimpl.
+    rewrite pow_pos_Pplus;simpl;rsimpl.
     add_push (P5 @ (tail l0));rrefl.
   rewrite H0;rsimpl.
   rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)).
   rewrite H;rewrite Pplus_comm.
-  rewrite pow_Pplus;rsimpl.
+  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) ->
@@ -725,11 +792,11 @@ Section MakeRingPol.
   rewrite jump_Pplus;rewrite IHP;rrefl.
   destruct p0;Esimpl2.
   rewrite IHP1;rewrite IHP2;simpl;rsimpl.
-  mul_push (pow (hd 0 l) p);rrefl.
+  mul_push (pow_pos rmul (hd 0 l) p);rrefl.
   rewrite IHP1;rewrite IHP2;simpl;rsimpl.
-  mul_push (pow (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
+  mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
   rewrite IHP1;simpl;rsimpl.
-  mul_push (pow (hd 0 l) p).
+  mul_push (pow_pos rmul (hd 0 l) p).
   rewrite H;rrefl.
  Qed.
 
@@ -741,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)).
@@ -753,12 +844,38 @@ 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,
    Mphi l (mkZmon j M) == Mphi l (zmon j M).
  intros M j l; case M; simpl; intros; rsimpl.
  Qed.
+ 
+ Lemma zmon_pred_ok : forall M j l, 
+    Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M).
+ Proof.
+   destruct j; simpl;intros auto; rsimpl.
+   rewrite mkZmon_ok;rsimpl.
+   rewrite mkZmon_ok;simpl. rewrite jump_Pdouble_minus_one; rsimpl.
+ Qed.
+
+ Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i.
+ Proof.
+  destruct M;simpl;intros;rsimpl.
+   rewrite zmon_pred_ok;simpl;rsimpl.
+  rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl.
+ Qed.
+
 
  Lemma Mphi_ok: forall P M l, 
     let (Q,R) := MFactor P M in
@@ -798,8 +915,7 @@ Section MakeRingPol.
      rewrite (ARadd_comm ARth); rsimpl.
      apply radd_ext; rsimpl.
      rewrite (ARadd_comm ARth); rsimpl.
-     case j; simpl; auto; try intros j1; rsimpl.
-     rewrite jump_Pdouble_minus_one; rsimpl.
+     rewrite zmon_pred_ok;rsimpl.
    intros j M1.
      case_eq ((i ?= j) Eq); intros He; simpl.
        rewrite (Pcompare_Eq_eq _ _ He).
@@ -827,7 +943,7 @@ Section MakeRingPol.
        apply rmul_ext; rsimpl.
        rewrite (ARmul_comm ARth); rsimpl.
        apply rmul_ext; rsimpl.
-       rewrite <- pow_Pplus.
+       rewrite <- pow_pos_Pplus.
        rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl.
        generalize (Hrec1 (mkZmon 1 M1) l); 
              case (MFactor P2 (mkZmon 1 M1));
@@ -847,13 +963,15 @@ Section MakeRingPol.
        repeat (rewrite <-(ARmul_assoc ARth)).
        rewrite (ARmul_comm ARth (Q3@l)); rsimpl.
        apply rmul_ext; rsimpl.
-       rewrite <- pow_Pplus.
+       rewrite <- pow_pos_Pplus.
        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.
@@ -864,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.
@@ -947,47 +1089,28 @@ Section MakeRingPol.
   | PEadd : PExpr -> PExpr -> PExpr
   | PEsub : PExpr -> PExpr -> PExpr
   | PEmul : PExpr -> PExpr -> PExpr
-  | PEopp : PExpr -> PExpr.
-
- (** normalisation towards polynomials *)
- 
- Definition X := (PX P1 xH P0).
-
- Definition mkX j :=
-  match j with
-  | xH => X
-  | xO j => Pinj (Pdouble_minus_one j) X
-  | xI j => Pinj (xO j) X
-  end.
+  | PEopp : PExpr -> PExpr
+  | PEpow : PExpr -> N -> PExpr.
 
- Fixpoint norm (pe:PExpr) : Pol :=
-  match pe with
-  | PEc c => Pc c
-  | PEX j => mkX j
-  | PEadd pe1 (PEopp pe2) => Psub (norm pe1) (norm pe2)
-  | PEadd (PEopp pe1) pe2 => Psub (norm pe2) (norm pe1)
-  | PEadd pe1 pe2 => Padd (norm pe1) (norm pe2)
-  | PEsub pe1 pe2 => Psub (norm pe1) (norm pe2)
-  | PEmul pe1 pe2 => Pmul (norm pe1) (norm pe2)
-  | PEopp pe1 => Popp (norm pe1)
-  end.
+ (** evaluation of polynomial expressions towards R *)
+ Definition mk_X j := mkPinj_pred j mkX.
 
  (** evaluation of polynomial expressions towards R *)
- 
+
  Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
-  match pe with
-  | PEc c => phi c
-  | 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)
-  | PEopp pe1 => - (PEeval l pe1)
-  end.
+   match pe with
+   | PEc c => phi c
+   | 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)
+   | PEopp pe1 => - (PEeval l pe1)
+   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
+   end.
 
  (** Correctness proofs *)
  
-
- Lemma mkX_ok : forall p l, nth 0 p l == (mkX p) @ l.
+ Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
  Proof.
   destruct p;simpl;intros;Esimpl;trivial.
   rewrite <-jump_tl;rewrite nth_jump;rrefl.
@@ -995,238 +1118,579 @@ Section MakeRingPol.
   rewrite nth_Pdouble_minus_one;rrefl.
  Qed.
 
- Lemma norm_PEopp : forall l pe,  (norm (PEopp pe))@l == -(norm pe)@l.
- Proof.
-  intros;simpl;apply Popp_ok.
- Qed.
-
  Ltac Esimpl3 := 
   repeat match goal with
   | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l)
   | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l)
-  | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe)
-  end;Esimpl2;try rrefl;try apply (ARadd_comm ARth).
+  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.
+  Variable n : nat.
+  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_aux (pe:PExpr) : Pol :=
+   match pe with
+   | PEc c => Pc c
+   | PEX j => mk_X j  
+   | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
+   | PEadd pe1 (PEopp pe2) => 
+     Psub (norm_aux pe1) (norm_aux pe2)
+   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
+   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
+   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) 
+   | PEopp pe1 => Popp (norm_aux pe1)
+   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
+   end.
 
- Lemma norm_ok : forall l pe,  PEeval l pe == (norm pe)@l.
- Proof.
-  induction pe;simpl;Esimpl3.
-  apply mkX_ok.
-  rewrite IHpe1;rewrite IHpe2; destruct pe1;destruct pe2;Esimpl3.
-  rewrite IHpe1;rewrite IHpe2;rrefl.
-  rewrite Pmul_ok;rewrite IHpe1;rewrite IHpe2;rrefl.
-  rewrite IHpe;rrefl.
- Qed.
+  Definition norm_subst pe := subst_l (norm_aux pe).
+
+ (* 
+  Fixpoint norm_subst (pe:PExpr) : Pol :=
+   match pe with
+   | PEc c => Pc c
+   | PEX j => subst_l (mk_X j)  
+   | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1)
+   | PEadd pe1 (PEopp pe2) => 
+     Psub (norm_subst pe1) (norm_subst pe2)
+   | PEadd pe1 pe2 => Padd (norm_subst  pe1) (norm_subst pe2)
+   | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2)
+   | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2) 
+   | PEopp pe1 => Popp (norm_subst pe1)
+   | PEpow pe1 n => Ppow_subst (norm_subst pe1) n
+   end.
 
- Lemma ring_correct : forall l pe1 pe2, 
-  ((norm pe1) ?== (norm pe2)) = true -> (PEeval l pe1) == (PEeval l pe2).
+  Lemma norm_subst_spec : 
+     forall l pe, MPcond lmp l ->
+       PEeval l pe == (norm_subst pe)@l. 
+  Proof.
+   intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). 
+      unfold subst_l;intros.
+      rewrite <- PNSubstL_ok;trivial. rrefl.
+   assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l).
+    intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl.
+   induction pe;simpl;Esimpl3.
+   rewrite subst_l_ok;apply mkX_ok.
+   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. 
+   rewrite IHpe1;rewrite IHpe2;rrefl.
+   rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl.
+   rewrite IHpe;rrefl.
+   unfold Ppow_subst. rewrite Ppow_N_ok. trivial.
+   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
+   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
+      repeat rewrite Pmul_ok;rrefl.
+  Qed.
+*)
+ Lemma norm_aux_spec : 
+     forall l pe, MPcond lmp l ->
+       PEeval l pe == (norm_aux pe)@l. 
+  Proof.
+   intros.
+   induction pe;simpl;Esimpl3.
+   apply mkX_ok.
+   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. 
+   rewrite IHpe1;rewrite IHpe2;rrefl.
+   rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
+   rewrite IHpe;rrefl.
+   rewrite Ppow_N_ok. intros;rrefl.
+   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
+   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
+      repeat rewrite Pmul_ok;rrefl.
+  Qed.
+
+ Lemma norm_subst_spec : 
+     forall l pe, MPcond lmp l ->
+       PEeval l pe == (norm_subst pe)@l.
  Proof.
-  intros l pe1 pe2 H.
-  repeat rewrite norm_ok.
-  apply  (Peq_ok (norm pe1) (norm pe2) H l).
- Qed.
-
-(** Evaluation function avoiding parentheses *)
- Fixpoint mkmult (r:R) (lm:list R) {struct lm}: R :=
-  match lm with
-  | nil => r
-  | cons h t => mkmult (r*h) t
-  end.
- 		       
- Definition mkadd_mult rP lm :=
-  match lm with
-  | nil => rP + 1
-  | cons h t => rP + mkmult h t
+  intros;unfold norm_subst.
+  unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial.
+ Qed. 
+ 
+ End NORM_SUBST_REC.
+  
+ Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop :=
+   match lpe with
+   | nil => True
+   | (me,pe)::lpe => 
+     match lpe with
+     | nil => PEeval l me == PEeval l pe
+     | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe
+     end
   end.
 
- Fixpoint powl (i:positive) (x:R) (l:list R) {struct i}: list R :=
-  match i with
-  | xH => cons x l
-  | xO i => powl i x (powl i x l)
-  | xI i => powl i x (powl i x (cons x l))
-  end.
-			       
- Fixpoint add_mult_dev (rP:R) (P:Pol) (fv lm:list R) {struct P} : R :=
-  (* rP + P@l * lm *)
+  Fixpoint mon_of_pol (P:Pol) : option Mon :=
   match P with
-  | Pc c => if c ?=! cI then mkadd_mult rP (rev' lm) 
-    else mkadd_mult rP (cons [c] (rev' lm))
-  | Pinj j Q => add_mult_dev rP Q (jump j fv) lm
-  | PX P i Q => 
-     let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in
-     if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm
+  | Pc c => if (c ?=! cI) then Some mon0 else None
+  | Pinj j P =>
+    match mon_of_pol P with 
+    | None => None
+    | Some m =>  Some (mkZmon j m) 
+    end
+  | PX P i Q =>
+    if Peq Q P0 then
+      match mon_of_pol P with
+      | None => None
+      | Some m => Some (mkVmon i m)
+      end
+    else None
   end.
- 
- Definition mkmult1 lm :=
-  match lm with
-  | nil => rI
-  | cons h t => mkmult h t
+
+ Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (Mon*Pol) :=
+  match lpe with
+  | nil => nil
+  | (me,pe)::lpe =>
+    match mon_of_pol (norm_subst 0 nil me) with
+    | None => mk_monpol_list lpe 
+    | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe 
+    end
   end.
+
+  Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m ->
+              forall l, Mphi l m == P@l.
+  Proof.
+    induction P;simpl;intros;Esimpl.  
+    assert (H1 := (morph_eq CRmorph) c cI).
+    destruct (c ?=! cI).
+    inversion H;rewrite H1;trivial;Esimpl.
+    discriminate.
+    generalize H;clear H;case_eq (mon_of_pol P);intros;try discriminate.
+    inversion H0.
+    rewrite mkZmon_ok;simpl;auto.
+    generalize H;clear H;change match P3 with
+        | Pc c => c ?=! cO
+        | Pinj _ _ => false
+        | PX _ _ _ => false
+        end with (P3 ?== P0).
+    assert (H := Peq_ok P3 P0).
+    destruct (P3 ?== P0).
+    case_eq (mon_of_pol P2);intros.
+    inversion H1.
+    rewrite mkVmon_ok;simpl.
+    rewrite H;trivial;Esimpl.  rewrite IHP1;trivial;Esimpl. discriminate.
+    intros;discriminate.
+   Qed.
+ 
+ Lemma interp_PElist_ok : forall l lpe, 
+         interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l.
+ Proof.
+   induction lpe;simpl. trivial.
+   destruct a;simpl;intros.
+   assert (HH:=mon_of_pol_ok (norm_subst 0 nil  p));
+     destruct  (mon_of_pol (norm_subst 0 nil p)).  
+   split.
+   rewrite <- norm_subst_spec. exact I.
+   destruct lpe;try destruct H;rewrite <- H;
+   rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial.
+   apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0.
+   apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0.
+ Qed.
+
+ Lemma norm_subst_ok : forall n l lpe pe,
+   interp_PElist l lpe ->
+   PEeval l pe == (norm_subst n (mk_monpol_list lpe) pe)@l.
+ Proof.
+   intros;apply norm_subst_spec. apply interp_PElist_ok;trivial.
+  Qed.
+ 
+ Lemma ring_correct : forall n l lpe pe1 pe2,
+   interp_PElist l lpe ->
+   (let lmp := mk_monpol_list lpe in
+   norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true ->
+   PEeval l pe1 == PEeval l pe2.
+ Proof.
+  simpl;intros.
+  do 2 (rewrite (norm_subst_ok n l lpe);trivial). 
+  apply Peq_ok;trivial.
+ Qed.  
+
+
+
+  (** Generic evaluation of polynomial towards R avoiding parenthesis *)
+ Variable get_sign : C -> option C.
+ Variable get_sign_spec : sign_theory ropp req phi get_sign.
+
+
+ Section EVALUATION.
+
+  (* [mkpow x p] = x^p *)
+  Variable mkpow : R -> positive -> R.
+  (* [mkpow x p] = -(x^p) *)
+  Variable mkopp_pow : R -> positive -> R.
+  (* [mkmult_pow r x p] = r * x^p *)
+  Variable mkmult_pow : R -> R -> positive -> R.
     
- Fixpoint mult_dev (P:Pol) (fv lm : list R) {struct P} : R :=
-  (* P@l * lm *)							      
+  Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R :=
+   match lm with
+   | nil => r
+   | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t 
+   end.
+
+  Definition mkmult1 lm :=
+   match lm with
+   | nil => 1
+   | cons (x,p) t => mkmult_rec (mkpow x p) t 
+   end.
+
+  Definition mkmultm1 lm :=
+   match lm with
+   | nil => ropp rI
+   | cons (x,p) t => mkmult_rec (mkopp_pow x p) t 
+   end.
+
+  Definition mkmult_c_pos c lm :=
+   if c ?=! cI then mkmult1 (rev' lm)
+   else mkmult_rec [c] (rev' lm).
+
+  Definition mkmult_c 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
+   | None => rP + mkmult_c_pos c lm
+   | Some c' => rP - mkmult_c_pos c' lm
+   end.
+
+  Definition add_pow_list (r:R) n l :=
+   match n with 
+   | N0 => l
+   | Npos p => (r,p)::l
+   end.
+
+  Fixpoint add_mult_dev 
+      (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R :=
+   match P with
+   | Pc c => 
+     let lm := add_pow_list (hd 0 fv) n lm in
+     mkadd_mult rP c lm
+   | Pinj j Q => 
+     add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
+   | PX P i Q => 
+     let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in
+     if Q ?== P0 then rP 
+     else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm)
+   end.
+
+  Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) 
+                     (lm:list (R*positive)) {struct P} : R :=
+  (* P@l * (hd 0 l)^n * lm *)						      
   match P with
-  | Pc c => if c ?=! cI then mkmult1 (rev' lm) else mkmult [c] (rev' lm)
-  | Pinj j Q => mult_dev Q (jump j fv) lm
+  | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm)
+  | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
   | PX P i Q => 
-     let rP := mult_dev P fv (powl i (hd 0 fv) lm) in
-     if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm
+     let rP := mult_dev P fv (Nplus (Npos i) n) lm in
+     if Q ?== P0 then rP 
+     else 
+       let lmq := add_pow_list (hd 0 fv) n lm in
+       add_mult_dev rP Q (tail fv) N0 lmq
   end. 
 
- Definition Pphi_dev fv P := mult_dev P fv nil.
+ Definition Pphi_avoid fv P := mult_dev P fv N0 nil.
+ 
+ Fixpoint r_list_pow (l:list (R*positive)) : R :=
+  match l with
+  | nil => rI
+  | cons (r,p) l => pow_pos rmul r p * r_list_pow l 
+  end.
 
- Add Morphism mkmult : mkmult_ext.
-  intros r r0 eqr l;generalize l r r0 eqr;clear l r r0 eqr;
-   induction l;simpl;intros.
-  trivial. apply IHl; rewrite eqr;rrefl.
- Qed.
+  Hypothesis mkpow_spec : forall r p, mkpow r p == pow_pos rmul r p.
+  Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). 
+  Hypothesis mkmult_pow_spec : forall r x p, mkmult_pow r x p == r * pow_pos rmul x p.
 
- Lemma mul_mkmult : forall lm r1 r2, r1 * mkmult r2 lm == mkmult (r1*r2) lm.
+ Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm.
  Proof.
-  induction lm;simpl;intros;try rrefl.
-  rewrite IHlm.
-  setoid_replace (r1 * (r2 * a)) with (r1 * r2 * a);Esimpl.
- Qed.
+   induction lm;intros;simpl;Esimpl.
+   destruct a as (x,p);Esimpl.
+   rewrite IHlm. rewrite mkmult_pow_spec. Esimpl.
+  Qed.
 
- Lemma mkmult1_mkmult : forall lm r, r * mkmult1 lm == mkmult r lm.
+ Lemma mkmult1_ok : forall lm, mkmult1 lm == r_list_pow lm.
  Proof.
-  destruct lm;simpl;intros. Esimpl.
-  apply mul_mkmult.
+   destruct lm;simpl;Esimpl.
+   destruct p. rewrite mkmult_rec_ok;rewrite mkpow_spec;Esimpl.
  Qed.
- 
- Lemma mkmult1_mkmult_1 : forall lm, mkmult1 lm == mkmult 1 lm.
+
+ Lemma mkmultm1_ok : forall lm, mkmultm1 lm == - r_list_pow lm.
  Proof.
-  intros;rewrite <- mkmult1_mkmult;Esimpl.
+  destruct lm;simpl;Esimpl.
+  destruct p;rewrite mkmult_rec_ok. rewrite mkopp_pow_spec;Esimpl.
  Qed.
 
- Lemma mkmult_rev_append : forall lm l r,
-  mkmult r (rev_append lm l) == mkmult (mkmult r l) lm.
+ Lemma r_list_pow_rev :  forall l, r_list_pow (rev' l) == r_list_pow l.
+ Proof.
+   assert 
+    (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l).
+   induction l;intros;simpl;Esimpl.
+   destruct a;rewrite IHl;Esimpl.
+   rewrite (ARmul_comm ARth (pow_pos rmul r p)). rrefl.
+  intros;unfold rev'. rewrite H;simpl;Esimpl.
+  Qed.
+
+ Lemma mkmult_c_pos_ok : forall c lm, mkmult_c_pos c lm == [c]* r_list_pow lm.
  Proof.
- induction lm; simpl in |- *; intros.
- rrefl.
- rewrite IHlm; simpl in |- *.
-   repeat rewrite <- (ARmul_comm ARth a); rewrite <- mul_mkmult.
-   rrefl.
+  intros;unfold mkmult_c_pos;simpl.
+   assert (H := (morph_eq CRmorph) c cI).
+   rewrite <- r_list_pow_rev; destruct (c ?=! cI). 
+  rewrite H;trivial;Esimpl.
+  apply mkmult1_ok.  apply mkmult_rec_ok.
  Qed.
 
- Lemma powl_mkmult_rev : forall p r x lm,
-  mkmult r (rev' (powl p x lm)) == mkmult (pow x p * r) (rev' lm).
+ Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm.
+ Proof.
+  intros;unfold mkmult_c;simpl.
+  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.
-  induction p;simpl;intros.
-  repeat rewrite IHp.
-  unfold rev';simpl.
-  repeat rewrite mkmult_rev_append.
-  simpl.
-  setoid_replace (pow x p * (pow x p * r) * x) 
-    with (x * pow x p * pow x p * r);Esimpl.
-  mul_push x;rrefl.
-  repeat rewrite IHp.
-  setoid_replace (pow x p * (pow x p * r) ) 
-    with (pow x p * pow x p * r);Esimpl.
-  unfold rev';simpl. repeat rewrite mkmult_rev_append;simpl.
-  rewrite (ARmul_comm ARth);rrefl.
+  intros;unfold mkadd_mult.
+  case_eq (get_sign c);intros.
+  rewrite (get_sign_spec.(sign_spec) _ H).
+  rewrite mkmult_c_pos_ok;Esimpl.
+  rewrite mkmult_c_pos_ok;Esimpl.
  Qed.
 
- Lemma Pphi_add_mult_dev : forall P rP fv lm, 
-    rP + P@fv * mkmult1 (rev' lm) == add_mult_dev rP P fv lm.
+ Lemma add_pow_list_ok : 
+      forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l.
  Proof.
-  induction P;simpl;intros.
-  assert (H := (morph_eq CRmorph) c cI).
-   destruct (c ?=! cI).
-    rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl.
-    destruct (rev' lm);Esimpl;rrefl.
-    rewrite mkmult1_mkmult;rrefl.
-   apply IHP.
-   replace (match P3 with
+   destruct n;simpl;intros;Esimpl.
+ Qed.
+
+ Lemma add_mult_dev_ok : forall P rP fv n lm, 
+    add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm.
+  Proof.
+    induction P;simpl;intros.  
+    rewrite mkadd_mult_ok. rewrite  add_pow_list_ok; Esimpl.
+    rewrite IHP. simpl. rewrite  add_pow_list_ok; Esimpl.
+    change (match P3 with
        | Pc c => c ?=! cO
        | Pinj _ _ => false
        | PX _ _ _ => false
-       end) with (Peq P3 P0);trivial.
+       end) with (Peq P3 P0).
+   change match n with
+    | N0 => Npos p
+    | Npos q => Npos (p + q)
+    end with (Nplus (Npos p) n);trivial.
    assert (H := Peq_ok P3 P0).
     destruct (P3 ?== P0).
-    rewrite (H (refl_equal true));simpl;Esimpl.
-   rewrite <- IHP1.
-     repeat rewrite mkmult1_mkmult_1.
-     rewrite powl_mkmult_rev.
-     rewrite <- mul_mkmult;Esimpl.
-   rewrite <- IHP2.
-   rewrite <- IHP1.
-     repeat rewrite mkmult1_mkmult_1.
-     rewrite powl_mkmult_rev.
-     rewrite <- mul_mkmult;Esimpl.
+    rewrite (H (refl_equal true)).
+   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+   rewrite  IHP2.
+   rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
  Qed.
-                                     
- Lemma Pphi_mult_dev : forall P fv lm,
-	 P@fv * mkmult1 (rev' lm) == mult_dev P fv lm.
+
+ Lemma mult_dev_ok : forall P fv n lm,    
+    mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm.
  Proof.
-  induction P;simpl;intros.
-   assert (H := (morph_eq CRmorph) c cI).
-   destruct (c ?=! cI).
-    rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl.
-    apply  mkmult1_mkmult.
-   apply IHP.
-   replace (match P3 with
+   induction P;simpl;intros;Esimpl.
+   rewrite mkmult_c_ok;rewrite add_pow_list_ok;Esimpl.
+   rewrite IHP. simpl;rewrite add_pow_list_ok;Esimpl.
+  change (match P3 with
        | Pc c => c ?=! cO
        | Pinj _ _ => false
        | PX _ _ _ => false
-       end) with (Peq P3 P0);trivial.
+       end) with (Peq P3 P0).
+   change match n with
+    | N0 => Npos p
+    | Npos q => Npos (p + q)
+    end with (Nplus (Npos p) n);trivial.
    assert (H := Peq_ok P3 P0).
-   destruct (P3 ?== P0).
-   rewrite (H (refl_equal true));simpl;Esimpl.
-   rewrite <- IHP1.
-     repeat rewrite mkmult1_mkmult_1.
-     rewrite powl_mkmult_rev.
-     rewrite <- mul_mkmult;Esimpl.
-   rewrite <- Pphi_add_mult_dev.
-   rewrite <- IHP1.
-     repeat rewrite mkmult1_mkmult_1.
-     rewrite powl_mkmult_rev.
-     rewrite <- mul_mkmult;Esimpl.
- Qed.
+    destruct (P3 ?== P0).
+    rewrite (H (refl_equal true)).
+   rewrite  IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+   rewrite add_mult_dev_ok. rewrite IHP1; rewrite add_pow_list_ok.
+   destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl.
+  Qed.
 
- Lemma Pphi_Pphi_dev :  forall P l,  P@l == Pphi_dev l P.
- Proof. 		
-  unfold Pphi_dev;intros.
-  rewrite <- Pphi_mult_dev;simpl;Esimpl.
+ Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P  == P@fv.
+ Proof.
+   unfold Pphi_avoid;intros;rewrite mult_dev_ok;simpl;Esimpl.
  Qed.
 
- Lemma Pphi_dev_gen_ok :  forall l pe,  PEeval l pe == Pphi_dev l (norm pe).
+ End EVALUATION.
+
+  Definition Pphi_pow := 
+   let mkpow x p := 
+      match p with xH => x | _ => rpow x (Cp_phi (Npos p)) end in
+   let mkopp_pow x p := ropp (mkpow x p)  in
+   let mkmult_pow r x p := rmul r (mkpow x p) in
+    Pphi_avoid mkpow mkopp_pow mkmult_pow.
+
+ Lemma local_mkpow_ok : 
+   forall (r : R) (p : positive),
+    match p with
+    | xI _ => rpow r (Cp_phi (Npos p))
+    | xO _ => rpow r (Cp_phi (Npos p))
+    | 1 => r
+    end == pow_pos rmul r p.
+ Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. Qed.
+ 
+ Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P  == P@fv.
  Proof.
-  intros l pe;rewrite <- Pphi_Pphi_dev;apply norm_ok.
+  unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;rrefl.
  Qed.
 
- Lemma Pphi_dev_ok :
-   forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
+ Lemma ring_rw_pow_correct : forall n lH l,  
+      interp_PElist l lH ->
+      forall lmp, mk_monpol_list lH = lmp ->
+      forall pe npe, norm_subst n lmp pe = npe ->
+      PEeval l pe == Pphi_pow l npe.
  Proof.
-  intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok.
- Qed. 
+  intros n lH l H1 lmp Heq1 pe npe Heq2.
+  rewrite Pphi_pow_ok. rewrite <- Heq2;rewrite <- Heq1.
+  apply norm_subst_ok. trivial.
+ Qed.
 
- Fixpoint MPcond_dev (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop :=            
-    match LM1 with 
-     cons (M1,P2) LM2 =>  (Mphi l M1 == Pphi_dev l P2) /\ (MPcond_dev LM2 l)
-    | _ => True
+ Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := 
+   match p with
+   | xH => r*x 
+   | xO p => mkmult_pow (mkmult_pow r x p) x p
+   | xI p => mkmult_pow (mkmult_pow (r*x) x p) x p
+   end.
+ 
+  Definition mkpow x p :=
+    match p with 
+    | xH => x
+    | xO p => mkmult_pow x x (Pdouble_minus_one p)
+    | xI p => mkmult_pow x x (xO p)
     end.
-
- Fixpoint MPcond_map (LM1: list (Mon * PExpr)): list (Mon * Pol) :=            
-    match LM1 with 
-     cons (M1,P2) LM2 =>  cons (M1, norm P2) (MPcond_map LM2)
-    | _ => nil
+ 
+  Definition mkopp_pow x p :=
+    match p with 
+    | xH => -x
+    | xO p => mkmult_pow (-x) x (Pdouble_minus_one p)
+    | xI p => mkmult_pow (-x) x (xO p)
     end.
 
- Lemma MP_cond_dev_imp_MP_cond: forall LM1 l,
-     MPcond_dev LM1 l -> MPcond LM1 l.
+  Definition Pphi_dev := Pphi_avoid mkpow mkopp_pow mkmult_pow.
+
+  Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p.
+  Proof.
+    induction p;intros;simpl;Esimpl.   
+    repeat rewrite IHp;Esimpl.
+    repeat rewrite IHp;Esimpl.
+  Qed.
+  
+ Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p.
+  Proof.
+    destruct p;simpl;intros;Esimpl.
+    repeat rewrite mkmult_pow_ok;Esimpl.
+    rewrite mkmult_pow_ok;Esimpl.
+    pattern x at 1;replace x with (pow_pos rmul x 1). 
+    rewrite <- pow_pos_Pplus. 
+    rewrite <- Pplus_one_succ_l.
+    rewrite Psucc_o_double_minus_one_eq_xO.
+    simpl;Esimpl.
+    trivial.
+  Qed.
+ 
+  Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p.
+  Proof.
+    destruct p;simpl;intros;Esimpl.
+    repeat rewrite mkmult_pow_ok;Esimpl.
+    rewrite mkmult_pow_ok;Esimpl.
+    pattern x at 1;replace x with (pow_pos rmul x 1). 
+    rewrite <- pow_pos_Pplus. 
+    rewrite <- Pplus_one_succ_l.
+    rewrite Psucc_o_double_minus_one_eq_xO.
+    simpl;Esimpl.
+    trivial.
+  Qed.
+
+ Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv.
+  Proof.
+   unfold Pphi_dev;intros;apply Pphi_avoid_ok.
+   intros;apply mkpow_ok.
+   intros;apply mkopp_pow_ok.
+   intros;apply mkmult_pow_ok.
+  Qed.
+
+ Lemma ring_rw_correct : forall n lH l,  
+      interp_PElist l lH ->
+      forall lmp, mk_monpol_list lH = lmp ->
+      forall pe npe, norm_subst n lmp pe = npe ->
+      PEeval l pe == Pphi_dev l npe.
  Proof.
- intros LM1; elim LM1; simpl; auto.
- intros (M2,P2) LM2 Hrec l [H1 H2]; split; auto.
- rewrite H1; rewrite Pphi_Pphi_dev; rsimpl. 
+  intros n lH l H1 lmp Heq1 pe npe Heq2.
+  rewrite  Pphi_dev_ok. rewrite <- Heq2;rewrite <- Heq1.
+  apply norm_subst_ok. trivial.
  Qed.
 
- Lemma PNSubstL_dev_ok: forall m n lm pe l,
-    let LM :=  MPcond_map lm in
-    MPcond_dev LM l -> PEeval l pe == Pphi_dev l (PNSubstL (norm pe) LM m n).
- intros m n lm p3 l LM H.
- rewrite <- Pphi_Pphi_dev; rewrite <- PNSubstL_ok; auto.
-   apply MP_cond_dev_imp_MP_cond; auto.
- rewrite Pphi_Pphi_dev; apply Pphi_dev_ok; auto.
- Qed.
 
-End MakeRingPol. 
+End MakeRingPol.
+
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 95efde7f..7419f184 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -3,16 +3,23 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import Ring_polynom.
 Require Import BinList.
+Require Import InitialRing.
 Declare ML Module "newring".
-
+  
 
 (* adds a definition id' on the normal form of t and an hypothesis id
    stating that t = id' (tries to produces a proof as small as possible) *)
 Ltac compute_assertion id  id' t :=
   let t' := eval vm_compute in t in
-  (pose (id' := t');
-   assert (id : t = id');
-   [exact_no_check (refl_equal id')|idtac]).
+  pose (id' := t');
+  assert (id : t = id');
+  [vm_cast_no_check (refl_equal id')|idtac].
+(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *)
+
+Ltac getGoal :=
+  match goal with 
+  | |- ?G => G
+  end.
 
 (********************************************************************)
 (* Tacticals to build reflexive tactics *)
@@ -23,7 +30,6 @@ Ltac OnEquation req :=
   | _ => fail 1 "Goal is not an equation (of expected equality)"
   end.
 
-
 Ltac OnMainSubgoal H ty :=
   match ty with
   | _ -> ?ty' =>
@@ -32,43 +38,54 @@ Ltac OnMainSubgoal H ty :=
   | _ => (fun tac => tac)
   end.
 
-Ltac ApplyLemmaAndSimpl tac lemma pe:=
-  let npe := fresh "ast_nf" in
+Ltac ApplyLemmaThen lemma expr tac :=
+  let nexpr := fresh "expr_nf" in
+  let H := fresh "eq_nf" in
+  let Heq := fresh "thm" in
+  let nf_spec :=
+    match type of (lemma expr) with
+      forall x, ?nf_spec = x -> _ => nf_spec
+    | _ => fail 1 "ApplyLemmaThen: cannot find norm expression"
+    end in
+  (compute_assertion H nexpr nf_spec;
+   (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
+   clear H;
+   OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr)).
+
+Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
+  let npe := fresh "expr_nf" in
   let H := fresh "eq_nf" in
   let Heq := fresh "thm" in
   let npe_spec :=
-    match type of (lemma pe) with
+    match type of (lemma expr) with
       forall npe, ?npe_spec = npe -> _ => npe_spec
-    | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression"
+    | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression"
     end in
   (compute_assertion H npe npe_spec;
    (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
    clear H;
    OnMainSubgoal Heq ltac:(type of Heq)
-     ltac:(tac Heq; rewrite Heq; clear Heq npe)).
+     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 *)
-Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl :=
-  let R := match type of req with ?R -> _ => R end in
-  (* build the atom list *)
-  let fv := list_fold_left FV_tac (@List.nil R) rl in
-  (* some type-checking to avoid late errors *)
-  (check_fv fv;
-   (* rewrite steps *)
-   list_iter
-     ltac:(fun r =>
-       let ast := SYN_tac r fv in
-       try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast)
-     rl).
+
+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 expr := SYN_tac term fv in
+      (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in
+     (* rewrite steps *)
+     lazy_list_fold_right fcons ltac:(idtac) terms in
+  LEMMA_tac fv RW_tac.
 
 (********************************************************)
 
-(* An object to return when an expression is not recognized as a constant *)
-Definition NotConstant := false.
-		      
+
 (* Building the atom list of a ring expression *)
-Ltac FV Cst add mul sub opp t fv :=
+Ltac FV Cst CstPow add mul sub opp pow t fv :=
  let rec TFV t fv :=
   match Cst t with
   | NotConstant =>
@@ -77,6 +94,11 @@ Ltac FV Cst add mul sub opp t fv :=
       | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (opp ?t1) => TFV t1 fv
+      | (pow ?t1 ?n) =>
+        match CstPow n with
+        | InitialRing.NotConstant => AddFvTail t fv
+        | _ => TFV t1 fv
+        end
       | _ => AddFvTail t fv
       end
   | _ => fv
@@ -84,10 +106,10 @@ Ltac FV Cst add mul sub opp t fv :=
  in TFV t fv.
 
  (* syntaxification of ring expressions *)
- Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := 
+Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := 
  let rec mkP t :=
     match Cst t with
-    | NotConstant =>
+    | InitialRing.NotConstant =>
         match t with 
         | (radd ?t1 ?t2) => 
           let e1 := mkP t1 in
@@ -100,6 +122,12 @@ Ltac FV Cst add mul sub opp t fv :=
           let e2 := mkP t2 in constr:(PEsub e1 e2)
         | (ropp ?t1) =>
           let e1 := mkP t1 in constr:(PEopp e1)
+        | (rpow ?t1 ?n) =>
+          match CstPow n with
+          | InitialRing.NotConstant => 
+            let p := Find_at t fv in constr:(PEX C p)
+          | ?c => let e1 := mkP t1 in constr:(PEpow e1 c)
+          end
         | _ =>
           let p := Find_at t fv in constr:(PEX C p)
         end
@@ -107,54 +135,222 @@ Ltac FV Cst add mul sub opp t fv :=
     end
  in mkP t.
 
+Ltac ParseRingComponents lemma :=
+  match type of lemma with
+  | context
+     [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+      (fun f => f R add mul sub opp pow C)
+  | _ => fail 1 "ring anomaly: bad correctness lemma (parse)"
+  end.
+
+
 (* ring tactics *)
 
- Ltac Ring Cst_tac lemma1 req :=
-  let Make_tac :=
-    match type of lemma1 with
-    | forall (l:list ?R) (pe1 pe2:PExpr ?C),
-      _ = true ->
-      req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ =>
-        let mkFV := FV Cst_tac add mul sub opp in
-        let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-        fun f => f R mkFV mkPol
-    | _ => fail 1 "ring anomaly: bad correctness lemma"
+Ltac FV_hypo_tac mkFV req lH :=
+  let R := match type of req with ?R -> _ => R end in
+  let FV_hypo_l_tac h :=
+    match h with @mkhypo (req ?pe _) _ => mkFV pe end in
+  let FV_hypo_r_tac h :=
+    match h with @mkhypo (req _ ?pe) _ => mkFV pe end in
+  let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in
+  list_fold_right FV_hypo_r_tac fv lH.
+
+Ltac mkHyp_tac C req mkPE lH :=
+  let mkHyp h res := 
+   match h with 
+   | @mkhypo (req ?r1 ?r2) _ =>
+     let pe1 := mkPE r1 in
+     let pe2 := mkPE r2 in
+     constr:(cons (pe1,pe2) res)
+   | _ => fail "hypothesis is not a ring equality"
+   end in
+  list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.
+     
+Ltac proofHyp_tac lH :=
+  let get_proof h :=
+    match h with
+    | @mkhypo _ ?p => p
     end in
-  let Main r1 r2 R mkFV mkPol :=
-    let fv := mkFV r1 (@List.nil R) in
-    let fv := mkFV r2 fv in
-    check_fv fv;
-    (let pe1 := mkPol r1 fv in
-     let pe2 := mkPol r2 fv in
-     apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring";
-     vm_compute;
-     exact (refl_equal true) || fail "not a valid ring equation") in
-  Make_tac ltac:(OnEquation req Main).
-
-Ltac Ring_simplify Cst_tac lemma2 req rl :=
-  let Make_tac :=
-    match type of lemma2 with 
-      forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C),
-      _ = npe ->
-      req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
-      let mkFV := FV Cst_tac add mul sub opp in
-      let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-      let simpl_ring H := protect_fv "ring" in H in
-      (fun tac => tac mkFV mkPol simpl_ring lemma2 req rl)
-    | _ => fail 1 "ring anomaly: bad correctness lemma"
+  let rec bh l :=
+    match l with
+    | nil => constr:(I)
+    | cons ?h nil => get_proof h
+    | cons ?h ?tl => 
+      let l := get_proof h in
+      let r := bh tl in  
+      constr:(conj l r)
     end in
-  Make_tac ReflexiveRewriteTactic.
+  bh lH.
+
+Definition ring_subst_niter := (10*10*10)%nat.
+ 
+Ltac Ring Cst_tac CstPow_tac lemma1 req n lH :=
+  let Main lhs rhs R radd rmul rsub ropp rpow C :=
+    let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in
+    let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in
+    let fv := FV_hypo_tac mkFV req lH in
+    let fv := mkFV lhs fv in
+    let fv := mkFV rhs fv in
+    check_fv fv;
+    let pe1 := mkPol lhs fv in
+    let pe2 := mkPol rhs fv in
+    let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+    let vlpe := fresh "hyp_list" in
+    let vfv := fresh "fv_list" in
+    pose (vlpe := lpe);
+    pose (vfv := fv);
+    (apply (lemma1 n vfv vlpe pe1 pe2)
+      || fail "typing error while applying ring");
+    [ ((let prh := proofHyp_tac lH in exact prh)
+        || idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial") 
+    | vm_compute;
+      (exact (refl_equal true) || fail "not a valid ring equation")] in
+  ParseRingComponents lemma1 ltac:(OnEquation req Main).
+
+Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
+  let Main R add mul sub opp pow C :=
+    let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in
+    let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in
+    let fv := FV_hypo_tac mkFV req lH in
+    let simpl_ring H := (protect_fv "ring" in H; f H) in
+    let Coeffs :=
+      match type of lemma2 with
+      | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] =>
+        (fun f => f cO cI cadd cmul csub copp ceqb)
+      | _ => fail 1 "ring_simplify anomaly: bad correctness lemma"
+      end in
+    let lemma_tac fv RW_tac := 
+      let rr_lemma := fresh "r_rw_lemma" in
+      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+      let vlpe := fresh "list_hyp" in
+      let vlmp := fresh "list_hyp_norm" in
+      let vlmp_eq := fresh "list_hyp_norm_eq" in
+      let prh := proofHyp_tac lH in
+      pose (vlpe := lpe);
+      Coeffs ltac:(fun cO cI cadd cmul csub copp ceqb =>
+        compute_assertion vlmp_eq vlmp 
+            (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe);
+        assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq)
+         || fail "type error when build the rewriting lemma";
+        RW_tac rr_lemma;
+        try clear rr_lemma vlmp_eq vlmp vlpe) in
+    ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in
+  ParseRingComponents lemma2 Main.
 
+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 lemma1 lemma2 pre post rl =>
-       pre(); Ring cst_tac lemma1 req).
+  let G := getGoal in ring_lookup Ring_gen [] [G].
+
+Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
+  let G := getGoal in ring_lookup Ring_gen [lH] [G].
+
+(* Simplification *)
+
+Ltac Ring_simplify_gen f :=
+  fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
+     let l := fresh "to_rewrite" in
+     pose (l:= rl);
+     generalize (refl_equal l);
+     unfold l at 2;
+     pre(); 
+     match goal with
+     | [|- l = ?RL -> _ ] =>
+       let Heq := fresh "Heq" in
+       intros Heq;clear Heq l;
+       Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL; 
+       post()
+     | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
+     end.
+
+Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
+
+Ltac Ring_nf Cst_tac lemma2 req rl f :=
+  let on_rhs H :=
+   match type of H with
+   | req _ ?rhs => clear H; f rhs
+   end in
+  Ring_norm_gen on_rhs Cst_tac lemma2 req rl.
+
+
+Tactic Notation (at level 0) 
+  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
+  let G := getGoal in ring_lookup Ring_simplify [lH] rl [G].
+
+Tactic Notation (at level 0) 
+  "ring_simplify" constr_list(rl) := 
+  let G := getGoal in ring_lookup Ring_simplify [] rl [G].
+
+
+Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=   
+ let G := getGoal in
+ 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.
+
+Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=   
+ let G := getGoal in
+ 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.
+
+
+(*
+
+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) := 
+  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.
+
+Tactic Notation (at level 0) 
+  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(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 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" 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].
 
-Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
-  ring_lookup
-    (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
-       pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl.
 
-(* A simple macro tactic to be prefered to ring_simplify *)
-Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
+*)
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index 2f7378eb..5498911d 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -7,6 +7,9 @@
 (************************************************************************)
 
 Require Import Setoid.
+Require Import BinPos.
+Require Import BinNat.
+
 Set Implicit Arguments.
 
 Module RingSyntax.
@@ -27,6 +30,71 @@ Reserved Notation "x == y" (at level 70, no associativity).
 End RingSyntax.
 Import RingSyntax.
 
+Section Power.
+ Variable R:Type.
+ Variable rI : R.
+ Variable rmul : R -> R -> R.
+ Variable req : R -> R -> Prop.
+ Variable Rsth : Setoid_Theory R req.
+ Notation "x * y " := (rmul x y).
+ Notation "x == y" := (req x y).
+
+ Hypothesis mul_ext : 
+   forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2.
+ Hypothesis mul_comm : forall x y, x * y == y * x.
+ Hypothesis mul_assoc  : forall x y z, x * (y * z) == (x * y) * z.
+ Add Setoid R req Rsth as R_set_Power.
+ Add Morphism rmul : rmul_ext_Power. exact mul_ext. Qed.
+
+
+ Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
+  match i with
+  | xH => x
+  | xO i => let p := pow_pos x i in rmul p p
+  | xI i => let p := pow_pos x i in rmul x (rmul p p)
+  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 (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.
+  repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
+  repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
+  apply (Seq_refl _ _ Rsth).
+ Qed.
+
+ Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+  intro x;induction i;intros.
+  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat rewrite IHi.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc.
+  simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc;
+   simpl. apply (Seq_refl _ _ Rsth).
+ Qed.
+
+ Definition pow_N (x:R) (p:N) := 
+  match p with
+  | N0 => rI
+  | Npos p => pow_pos x p
+  end. 
+
+ Definition id_phi_N (x:N) : N := x.
+
+ Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.
+ Proof.
+  intros; apply (Seq_refl _ _ Rsth).
+ Qed.
+
+End Power.
+
 Section DEFINITIONS.
  Variable R : Type.
  Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
@@ -126,6 +194,19 @@ Section DEFINITIONS.
     morph_opp : forall x, [-!x] == -[x];
     morph_eq  : forall x y, x?=!y = true -> [x] == [y] 
   }.
+
+ Section SIGN.
+  Variable get_sign : C -> option C.
+  Record sign_theory : Prop := mksign_th {
+    sign_spec : forall c c', get_sign c = Some c' -> [c] == - [c']
+  }.
+ End SIGN.
+
+ Definition get_sign_None (c:C) := @None C.
+
+ Lemma get_sign_None_th : sign_theory get_sign_None.
+ Proof. constructor;intros;discriminate. Qed.
+
  End MORPHISM. 
 
  (** Identity is a morphism *)
@@ -140,6 +221,20 @@ Section DEFINITIONS.
   try apply (Seq_refl _ _ Rsth);auto.
  Qed.
 
+ (** Specification of the power function *)
+ Section POWER.
+  Variable Cpow : Set.
+  Variable Cp_phi : N -> Cpow.
+  Variable rpow : R -> Cpow -> R. 
+  
+  Record power_theory : Prop := mkpow_th {
+    rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
+  }.
+
+ End POWER.
+
+ Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth).
+
 End DEFINITIONS.
 
 
@@ -437,11 +532,12 @@ Qed.
 
 End ALMOST_RING.
 
+
 Section AddRing.
 
- Variable R : Type.
+(* Variable R : Type.
  Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable req : R -> R -> Prop.
+ Variable req : R -> R -> Prop. *)
 
 Inductive ring_kind : Type :=
 | Abstract
@@ -461,6 +557,7 @@ 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/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4f47fff0..8de7021e 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -8,26 +8,49 @@
 
 Require Export Ring.
 Require Import ZArith_base.
+Require Import Zpow_def.
+
 Import InitialRing.
 
 Set Implicit Arguments.
 
-Ltac isZcst t :=
-  let t := eval hnf in t in
-  match t with
-    Z0 => constr:true
-  | Zpos ?p => isZcst p
-  | Zneg ?p => isZcst p
-  | xI ?p => isZcst p
-  | xO ?p => isZcst p
-  | xH => constr:true
-  | _ => constr:false
-  end.
 Ltac Zcst t :=
   match isZcst t with
     true => t
   | _ => NotConstant
   end.
 
+Ltac isZpow_coef t :=
+  match t with 
+  | Zpos ?p => isPcst p
+  | Z0 => true
+  | _ => false
+  end.
+
+Definition N_of_Z x :=
+ match x with
+ | Zpos p => Npos p
+ | _ => N0
+ end.
+
+Ltac Zpow_tac t :=
+ match isZpow_coef t with
+ | true => constr:(N_of_Z t)
+ | _ => constr:(NotConstant)
+ end.
+
+Ltac Zpower_neg :=
+  repeat match goal with
+  | [|- ?G] => 
+    match G with 
+    | context c [Zpower _ (Zneg _)] =>
+      let t := context c [Z0] in
+      change t
+    end
+  end.   
+
+
 Add Ring Zr : Zth
-  (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]).
+  (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 daa2fedb..8b2ce26b 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: newring.ml4 9603 2007-02-07 00:41:16Z barras $ i*)
 
 open Pp
 open Util
@@ -127,6 +127,12 @@ TACTIC EXTEND closed_term
     [ closed_term t l ]
 END
 ;;
+
+TACTIC EXTEND echo 
+| [ "echo" constr(t) ] -> 
+  [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
+END;;
+
 (*
 let closed_term_ast l =
   TacFun([Some(id_of_string"t")],
@@ -196,7 +202,8 @@ let constr_of = function
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
-   ["Coq";"Lists";"List"]
+   ["Coq";"Lists";"List"];
+   ["Coq";"Init";"Datatypes"]
   ]
 
 let coq_constant c =
@@ -205,18 +212,24 @@ let coq_constant 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 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 *)
@@ -265,11 +278,18 @@ let coq_mk_seqe = my_constant "mk_seqe"
 
 let ltac_inv_morphZ = zltac"inv_gen_phiZ"
 let ltac_inv_morphN = zltac"inv_gen_phiN"
-
 let coq_abstract = my_constant"Abstract"
 let coq_comp = my_constant"Computational"
 let coq_morph = my_constant"Morphism"
 
+(* power function *)
+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"
+
 (* Equality: do not evaluate but make recursive call on both sides *)
 let map_with_eq arg_map c =
   let (req,_,_) = dest_rel c in
@@ -283,10 +303,12 @@ 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|6|7|8|9|11->Eval|10->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|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->Eval|8->Rec|_->Prot)])
+    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -299,6 +321,7 @@ type ring_info =
       ring_morph : constr;
       ring_th : constr;
       ring_cst_tac : glob_tactic_expr;
+      ring_pow_tac : glob_tactic_expr;
       ring_lemma1 : constr;
       ring_lemma2 : constr;
       ring_pre_tac : glob_tactic_expr;
@@ -316,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
@@ -337,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"
@@ -378,6 +402,7 @@ let subst_th (_,subst,th) =
   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
   if c' == th.ring_carrier &&
@@ -389,6 +414,7 @@ let subst_th (_,subst,th) =
      thm1' == th.ring_lemma1 &&
      thm2' == th.ring_lemma2 &&
      tac' == th.ring_cst_tac &&
+     pow_tac' == th.ring_pow_tac &&
      pretac' == th.ring_pre_tac &&
      posttac' == th.ring_post_tac then th
   else
@@ -399,6 +425,7 @@ let subst_th (_,subst,th) =
       ring_morph = morph';
       ring_th = th';
       ring_cst_tac = tac';
+      ring_pow_tac = pow_tac';
       ring_lemma1 = thm1';
       ring_lemma2 = thm2';
       ring_pre_tac = pretac';
@@ -532,14 +559,50 @@ let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac =
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | _ -> error"a tactic must be specified for an almost_ring")
 
-let add_theory name rth eqth morphth cst_tac (pre,post) =
+let make_hyp env c =
+  let t = (Typeops.typing env c).uj_type 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
+  match pow with
+  | None -> 
+      let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
+      (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+  | Some (tac, spec) -> 
+      let tac = 
+        match tac with
+        | CstTac t -> Tacinterp.glob_tactic t
+        | Closed lc -> closed_term_ast (List.map Nametab.global lc) in
+      let spec = make_hyp env (ic spec) in
+      (tac, lapp coq_Some [|carrier; spec|])
+
+let interp_sign env sign =
+  let carrier = Lazy.force coq_hypo in
+  match sign with
+  | None -> lapp coq_None [|carrier|] 
+  | Some spec -> 
+      let spec = make_hyp env (ic spec) in
+      lapp coq_Some [|carrier;spec|]
+       (* Same remark on ill-typed terms ... *)
+
+let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
   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 rk = reflect_coeff morphth in
   let params =
-    exec_tactic env 5 (zltac"ring_lemmas") (List.map carg[sth;ext;rth;rk]) in
+    exec_tactic env 5 (zltac "ring_lemmas") 
+      (List.map carg[sth;ext;rth;pspec;sspec;rk]) in
   let lemma1 = constr_of params.(3) in
   let lemma2 = constr_of params.(4) in
 
@@ -564,6 +627,7 @@ let add_theory name rth eqth morphth cst_tac (pre,post) =
           ring_morph = constr_of params.(2);
           ring_th = constr_of params.(0);
           ring_cst_tac = cst_tac;
+	  ring_pow_tac = pow_tac;
           ring_lemma1 = lemma1;
           ring_lemma2 = lemma2;
           ring_pre_tac = pretac;
@@ -576,6 +640,10 @@ type ring_mod =
   | 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
+           (* Syntaxification tactic , correctness lemma *)
+  | Sign_spec of Topconstr.constr_expr
+
 
 VERNAC ARGUMENT EXTEND ring_mod
   | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ]
@@ -586,6 +654,11 @@ VERNAC ARGUMENT EXTEND ring_mod
   | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
   | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ]
   | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ]
+  | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ]
+  | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
+           [ Pow_spec (Closed l, pow_spec) ]   
+  | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
+           [ Pow_spec (CstTac cst_tac, pow_spec) ]
 END
 
 let set_once s r v =
@@ -597,45 +670,54 @@ let process_ring_mods l =
   let cst_tac = ref None in
   let pre = ref None in
   let post = ref None in
+  let sign = ref None in
+  let power = ref None in
   List.iter(function
       Ring_kind k -> set_once "ring kind" kind 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)) l;
+    | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext) 
+    | Pow_spec(t,spec) -> set_once "power" power (t,spec)
+    | Sign_spec t -> set_once "sign" sign t) l;
   let k = match !kind with Some k -> k | None -> Abstract in
-  (k, !set, !cst_tac, !pre, !post)
+  (k, !set, !cst_tac, !pre, !post, !power, !sign)
 
 VERNAC COMMAND EXTEND AddSetoidRing
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
-    [ let (k,set,cst,pre,post) = process_ring_mods l in
-      add_theory id (ic t) set k cst (pre,post) ]
+    [ let (k,set,cst,pre,post,power,sign) = process_ring_mods l in
+      add_theory id (ic t) set k cst (pre,post) power sign ]
 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) 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
   let ext = carg e.ring_ext in
   let morph = carg e.ring_morph in
   let th = carg e.ring_th in
   let cst_tac = Tacexp e.ring_cst_tac in
+  let pow_tac = Tacexp e.ring_pow_tac in
   let lemma1 = carg e.ring_lemma1 in
   let lemma2 = carg e.ring_lemma2 in
   let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in
@@ -644,12 +726,17 @@ let ring_lookup (f:glob_tactic_expr) rl gl =
     (TacLetIn
       ([(dummy_loc,id_of_string"f"),None,Tacexp f],
        ltac_lcall "f"
-         [req;sth;ext;morph;th;cst_tac;lemma1;lemma2;pretac;posttac;rl])) gl
+         [req;sth;ext;morph;th;cst_tac;pow_tac;
+          lemma1;lemma2;pretac;posttac;lH;rl])) gl
 
 TACTIC EXTEND ring_lookup
-| [ "ring_lookup" tactic(f) constr_list(l) ] -> [ ring_lookup (fst f) l ]
+| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)
+      "[" constr(t) "]" ] ->
+          [ring_lookup (fst f) lH lr t]
 END
 
+
+ 
 (***********************************************************************)
 
 let new_field_path =
@@ -666,14 +753,20 @@ 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|7|8|9|10|12|13->Eval|11->Rec|_->Prot);
-    (* Pphi_dev: evaluate polynomial and coef operations, protect
+      (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
+    my_constant "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 *)
-    my_constant "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->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|13|15|17->Eval|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring 
        operations and make recursive call on the var map *)
-    my_constant "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);;
-
+    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)]);;
 
 let _ = add_map "field_cond"
   (map_with_eq
@@ -681,7 +774,8 @@ let _ = add_map "field_cond"
      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->Eval|9->Rec|_->Prot)]);;
+     my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);;
+(*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
 
 
 let afield_theory = my_constant "almost_field_theory"
@@ -715,9 +809,11 @@ type field_info =
     { field_carrier : types;
       field_req : constr;
       field_cst_tac : glob_tactic_expr;
+      field_pow_tac : glob_tactic_expr;
       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 }
@@ -734,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, _ ->
@@ -756,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"
@@ -796,8 +892,10 @@ 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
   let posttac'= subst_tactic subst th.field_post_tac in
   if c' == th.field_carrier &&
@@ -805,18 +903,22 @@ 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 &&
      posttac' == th.field_post_tac then th
   else
     { field_carrier = c';
       field_req = eq';
       field_cst_tac = tac';
+      field_pow_tac = pow_tac';
       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' }
 
@@ -850,30 +952,34 @@ let default_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) =
+let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
   let env = Global.env() in
   let sigma = Evd.empty 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
   let eqth = Some(sth,ext) in
-  let _ = add_theory name rth eqth morphth cst_tac (None,None) in
+  let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign in
+  let (pow_tac, pspec) = interp_power env power in 
+  let sspec = interp_sign env sign in
   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")
-      (List.map carg[sth;ext;inv_m;fth;rk]) in
+    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
@@ -889,9 +995,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) =
         { field_carrier = r;
           field_req = req;
           field_cst_tac = cst_tac;
+          field_pow_tac = pow_tac;
           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  ()
@@ -902,7 +1010,7 @@ type field_mod =
 
 VERNAC ARGUMENT EXTEND field_mod
   | [ ring_mod(m) ] -> [ Ring_mod m ]
-  | [ "infinite" constr(inj) ] -> [ Inject inj ]
+  | [ "completeness" constr(inj) ] -> [ Inject inj ]
 END
 
 let process_field_mods l =
@@ -911,7 +1019,9 @@ let process_field_mods l =
   let cst_tac = ref None in
   let pre = ref None in
   let post = ref None in
-  let inj = ref None in
+  let inj = ref None in  
+  let sign = ref None in
+  let power = ref None in
   List.iter(function
       Ring_mod(Ring_kind k) -> set_once "field kind" kind k
     | Ring_mod(Const_tac t) ->
@@ -919,26 +1029,32 @@ let process_field_mods l =
     | 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(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
+    | Ring_mod(Sign_spec t) -> set_once "sign" sign t
     | Inject i -> set_once "infinite property" inj (ic i)) l;
   let k = match !kind with Some k -> k | None -> Abstract in
-  (k, !set, !inj, !cst_tac, !pre, !post)
+  (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign)
 
 VERNAC COMMAND EXTEND AddSetoidField
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> 
-  [ let (k,set,inj,cst_tac,pre,post) = process_field_mods l in
-    add_field_theory id (ic t) set k cst_tac inj (pre,post) ]
+  [ let (k,set,inj,cst_tac,pre,post,power,sign) = process_field_mods l in
+    add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign]
 END
 
-let field_lookup (f:glob_tactic_expr) 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
+  let pow_tac = Tacexp e.field_pow_tac in
   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
@@ -946,9 +1062,11 @@ let field_lookup (f:glob_tactic_expr) rl gl =
     (TacLetIn
       ([(dummy_loc,id_of_string"f"),None,Tacexp f],
        ltac_lcall "f"
-         [req;cst_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok;
-          pretac;posttac;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(l) ] -> [ field_lookup (fst f) l ]
+| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) 
+     "[" constr(t) "]" ] -> 
+      [ field_lookup (fst f) lH l t ]
 END