Fixing an incompleteness of the ring/field tactics

The problem occurs when a customized ring/field structure       
declared with a so-called "morphism" (see 24.5 in the manual) tactic
allowing to reify (numerical) constants efficiently.

When declaring a ring/field structure, the user can provide a cast 
function phi in order to express numerical constants in another type than 
the carrier of the ring. This is useful for instance when the ring is
abstract (like the type R of reals) and one needs to express constants
to large to be parsed in unary representation (for instance using a
phi : Z -> R).

Formerly, the completeness of the tactic required (phi 1) (resp. (phi 0))
to be convertible to 1 (resp. 0), which is not the case when phi is
opaque. This was not documented untill recently
but I moreover think this is also not desirable
since the user can have good reasons to work with such an opaque case phi.

Hence this commit:
- adds two constructors to PExpr and FExpr for a correct reification
- unplugs the optimizations in reification: optimizing reification 
  is much less efficient than using a cast known to the tactic.

TODO : It would probably be worth declaring IZR as a cast in the ring/field
tactics provided for Reals in the std lib.

The completeness of the tactic formerly relied on the fact that 


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

9 files changed, 137 insertions, 94 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 21a94afca4..2a287556be 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -98,7 +98,7 @@ Definition PhiR : list R -> PolZ -> R :=
     (InitialRing.gen_phiZ ring0 ring1 add mul opp)).
 
 Definition PEevalR : list R -> PEZ -> R :=
-   PEeval ring0 add mul sub opp
+   PEeval ring0 ring1 add mul sub opp
     (gen_phiZ ring0 ring1 add mul opp)
          N.to_nat pow.
 
@@ -241,6 +241,8 @@ Fixpoint interpret3 t fv {struct t}: R :=
   | (PEpow t1 t2) =>
        let v1  := interpret3 t1 fv in pow v1 (N.to_nat t2)
   | (PEc t1) => (IZR1 t1)
+  | PEO => 0
+  | PEI => 1
   | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0
   end.
 
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 02194d4f10..cb2e78e427 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -21,6 +21,7 @@ Require Export Ncring_tac.
 Class Cring {R:Type}`{Rr:Ring R} := 
  cring_mul_comm: forall x y:R, x * y == y * x.
 
+
 Ltac reify_goal lvar lexpr lterm:=
   (*idtac lvar; idtac lexpr; idtac lterm;*)
   match lexpr with
@@ -30,10 +31,10 @@ Ltac reify_goal lvar lexpr lterm:=
           |- (?op ?u1 ?u2) =>
            change (op 
              (@Ring_polynom.PEeval
-               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
                (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
              (@Ring_polynom.PEeval
-               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
                (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
         end
   end.
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index dda1edbe14..1b52be14b3 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -10,12 +10,19 @@ Require Import Ring_tac BinList Ring_polynom InitialRing.
 Require Export Field_theory.
 
  (* syntaxification *)
- Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+ Ltac mkFieldexpr C Cst CstPow rO rI radd rmul rsub ropp rdiv rinv rpow t fv :=
  let rec mkP t :=
     let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with
+        | rO => 
+          fun _ => constr:(@FEO C)
+        | rI => 
+          fun _ => constr:(@FEI C)
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
@@ -54,11 +61,16 @@ Require Export Field_theory.
     f ()
  in mkP t.
 
-Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac FFV Cst CstPow rO rI add mul sub opp div inv pow t fv :=
  let rec TFV t fv :=
   match Cst t with
   | InitialRing.NotConstant =>
       match t with
+      | rO => fv
+      | rI => fv
       | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
@@ -83,60 +95,60 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
 Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post :=
   let FLD :=
     match type of L1 with
-    | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
+    | context [req (@FEeval ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
                                       ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
         (fun proj =>
            proj Cst_tac Pow_tac pre post
-             req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
+             req rO rI radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
     | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
     end in
   F FLD.
 
 Ltac get_FldPre FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        pre).
 
 Ltac get_FldPost FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        post).
 
 Ltac get_L1 FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L1).
 
 Ltac get_SimplifyEqLemma FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L2).
 
 Ltac get_SimplifyLemma FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L3).
 
 Ltac get_L4 FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        L4).
 
 Ltac get_CondLemma FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        cond_ok).
 
 Ltac get_FldEq FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
        req).
 
@@ -146,33 +158,33 @@ Ltac get_FldCarrier FLD :=
 
 Ltac get_RingFV FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       FV Cst_tac Pow_tac radd rmul rsub ropp rpow).
+       FV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
 
 Ltac get_FFV FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+       FFV Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
 
 Ltac get_RingMeta FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow).
+       mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow).
 
 Ltac get_Meta FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+       mkFieldexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rdiv rinv rpow).
 
 Ltac get_Hyp_tac FLD :=
   FLD ltac:
-      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+      (fun Cst_tac Pow_tac pre post req r0 r1 radd rmul rsub ropp rdiv rinv rpow C
            L1 L2 L3 L4 cond_ok =>
-       let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
+       let mkPol := mkPolexpr C Cst_tac Pow_tac r0 r1 radd rmul rsub ropp rpow in
        fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
 
 Ltac get_FEeval FLD :=
@@ -180,8 +192,8 @@ Ltac get_FEeval FLD :=
   match type of L1 with
   | context
     [(@FEeval
-      ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
-       constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow)
+      ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
+       constr:(@FEeval R r0 r1 add mul sub opp div inv C phi Cpow powphi pow)
   | _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)"
   end.
 
@@ -560,7 +572,7 @@ Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
              (fun f =>
                f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
                   cond1_ok cond2_ok)
-           | _ => fail 4 "field: bad coefficiant division specification"
+           | _ => fail 4 "field: bad coefficient division specification"
            end
          | _ => fail 3 "field: bad sign specification"
          end
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index bc947d54e8..4c9b34b6ab 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -135,7 +135,7 @@ Let rpow_pow := pow_th.(rpow_pow_N).
 Bind Scope PE_scope with PExpr.
 Delimit Scope PE_scope with poly.
 
-Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
+Notation NPEeval := (PEeval rO rI radd rmul rsub ropp phi Cp_phi rpow).
 Notation "P @ l" := (NPEeval l P) (at level 10, no associativity).
 
 Infix "+" := PEadd : PE_scope.
@@ -698,6 +698,8 @@ Fixpoint PEsimp (e : PExpr C) : PExpr C :=
 Theorem PEsimp_ok e : (PEsimp e === e)%poly.
 Proof.
 induction e; simpl.
+- reflexivity.
+- reflexivity.
 - intro l; trivial.
 - intro l; trivial.
 - rewrite NPEadd_ok. now f_equiv.
@@ -717,7 +719,9 @@ Qed.
 (* The input: syntax of a field expression *)
 
 Inductive FExpr : Type :=
-   FEc: C ->  FExpr
+ | FEO : FExpr
+ | FEI : FExpr
+ | FEc: C ->  FExpr
  | FEX: positive ->  FExpr
  | FEadd: FExpr -> FExpr ->  FExpr
  | FEsub: FExpr -> FExpr ->  FExpr
@@ -729,6 +733,8 @@ Inductive FExpr : Type :=
 
 Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
   match pe with
+  | FEO       => rO
+  | FEI       => rI
   | FEc c     => phi c
   | FEX x     => BinList.nth 0 x l
   | FEadd x y => FEeval l x + FEeval l y
@@ -1024,6 +1030,8 @@ Qed.
 
 Fixpoint Fnorm (e : FExpr) : linear :=
   match e with
+  | FEO => mk_linear (PEc cO) (PEc cI) nil
+  | FEI => mk_linear (PEc cI) (PEc cI) nil
   | FEc c => mk_linear (PEc c) (PEc cI) nil
   | FEX x => mk_linear (PEX C x) (PEc cI) nil
   | FEadd e1 e2 =>
@@ -1083,6 +1091,8 @@ Theorem Pcond_Fnorm l e :
 Proof.
 induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
  simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
+- simpl. rewrite phi_1; exact rI_neq_rO.
+- simpl. rewrite phi_1; exact rI_neq_rO.
 - simpl; intros. rewrite phi_1; exact rI_neq_rO.
 - simpl; intros. rewrite phi_1; exact rI_neq_rO.
 - rewrite <- split_ok_r. simpl. apply field_is_integral_domain.
@@ -1125,6 +1135,8 @@ induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
  try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2);
  try set (F1 := Fnorm fe1) in *; try set (F2 := Fnorm fe2) in *.
 
+- now rewrite phi_1, phi_0, rdiv_def.
+- now rewrite phi_1; apply rdiv1.
 - rewrite phi_1; apply rdiv1.
 - rewrite phi_1; apply rdiv1.
 - rewrite NPEadd_ok, !NPEmul_ok. simpl.
@@ -1177,7 +1189,7 @@ apply cross_product_eq; trivial;
 Qed.
 
 (* Correctness lemmas of reflexive tactics *)
-Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow).
+Notation Ninterp_PElist := (interp_PElist rO rI radd rmul rsub ropp req phi Cp_phi rpow).
 Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
 
 Theorem Fnorm_ok:
@@ -1747,3 +1759,6 @@ Qed.
 End Field.
 
 End Complete.
+
+Arguments FEO [C].
+Arguments FEI [C].
\ No newline at end of file
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 7ffe98e296..32824838bc 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -416,8 +416,11 @@ Qed.
  Variable pow_th : power_theory Cp_phi rpow.
 
  (** evaluation of polynomial expressions towards R *)
+
  Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
    match pe with
+   | PEO => 0
+   | PEI => 1
    | PEc c => [c]
    | PEX _ j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
@@ -500,6 +503,8 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
 
   Fixpoint norm_aux (pe:PExpr C) : Pol :=
    match pe with
+   | PEO => Pc cO
+   | PEI => Pc cI
    | PEc c => Pc c
    | PEX _ j => mk_X j
    | PEadd pe1 (PEopp pe2) =>
@@ -520,28 +525,30 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
   Proof.
    intros.
    induction pe.
-Esimpl3. Esimpl3. simpl.
- rewrite IHpe1;rewrite IHpe2.
- destruct pe2; Esimpl3. 
-unfold Psub.
-destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
-simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
-destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity.
-Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
- Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
-simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
-simpl. rewrite IHpe; Esimpl3. 
-simpl.
-   rewrite Ppow_N_ok; (intros;try reflexivity). 
-   rewrite rpow_pow_N.  Esimpl3.
-   induction n;simpl. Esimpl3. induction p; simpl.
-  try rewrite IHp;try rewrite IHpe;
- repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;reflexivity.
-rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe;
- repeat rewrite Pms_ok;
-      repeat rewrite Pmul_ok;reflexivity. trivial.
-exact pow_th.
+   - now simpl; rewrite <- ring_morphism0.
+   - now simpl; rewrite <- ring_morphism1.
+   - Esimpl3. 
+   - Esimpl3. 
+   - simpl.
+     rewrite IHpe1;rewrite IHpe2.
+     destruct pe2; Esimpl3. 
+     unfold Psub.
+     destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
+   - simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
+     now destruct pe1; 
+       [destruct pe2; rewrite Padd_ok; rewrite Popp_ok; Esimpl3 | Esimpl3..]. 
+   - simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
+   - now simpl; rewrite IHpe; Esimpl3. 
+   - simpl.
+     rewrite Ppow_N_ok; (intros;try reflexivity). 
+     rewrite rpow_pow_N; [| now apply pow_th]. 
+     induction n;simpl; [now Esimpl3|]. 
+     induction p; simpl; trivial.
+     + try rewrite IHp;try rewrite IHpe;
+         repeat rewrite Pms_ok; repeat rewrite Pmul_ok;reflexivity.
+     + rewrite Pmul_ok. 
+       try rewrite IHp;try rewrite IHpe; repeat rewrite Pms_ok;
+         repeat rewrite Pmul_ok;reflexivity. 
   Qed.
 
  Lemma norm_subst_spec :
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
index 804c62d589..53fd202ef2 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -127,7 +127,6 @@ Definition list_reifyl (R:Type) lexpr lvar lterm
 
 Unset Implicit Arguments.
 
-
 Ltac lterm_goal g :=
   match g with
   | ?t1 == ?t2 => constr:(t1::t2::nil)
@@ -138,6 +137,7 @@ Ltac lterm_goal g :=
 Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
  intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. 
 
+
 Ltac reify_goal lvar lexpr lterm:=
   (*idtac lvar; idtac lexpr; idtac lterm;*)
   match lexpr with
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index eeae7077d7..6ffa548661 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -896,6 +896,8 @@ Section MakeRingPol.
  (** Definition of polynomial expressions *)
 
  Inductive PExpr : Type :=
+  | PEO : PExpr
+  | PEI : PExpr            
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
   | PEadd : PExpr -> PExpr -> PExpr
@@ -904,6 +906,7 @@ Section MakeRingPol.
   | PEopp : PExpr -> PExpr
   | PEpow : PExpr -> N -> PExpr.
 
+
  (** evaluation of polynomial expressions towards R *)
  Definition mk_X j := mkPinj_pred j mkX.
 
@@ -911,6 +914,8 @@ Section MakeRingPol.
 
  Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
    match pe with
+   | PEO => rO
+   | PEI => rI
    | PEc c => phi c
    | PEX j => nth 0 j l
    | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
@@ -979,6 +984,8 @@ Section POWER.
 
   Fixpoint norm_aux (pe:PExpr) : Pol :=
    match pe with
+   | PEO => Pc cO
+   | PEI => Pc cI
    | PEc c => Pc c
    | PEX j => mk_X j
    | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1)
@@ -1010,7 +1017,7 @@ Section POWER.
     end.
   Proof.
   simpl (norm_aux (PEadd _ _)).
-  destruct pe1; [ | | | | | reflexivity | ];
+  destruct pe1; [ | | | | | | | reflexivity | ];
    destruct pe2; simpl get_PEopp; reflexivity.
   Qed.
 
@@ -1028,6 +1035,8 @@ Section POWER.
   Proof.
    intros.
    induction pe.
+   - now rewrite (morph0 CRmorph).
+   - now rewrite (morph1 CRmorph).
    - reflexivity.
    - apply mkX_ok.
    - simpl PEeval. rewrite IHpe1, IHpe2.
@@ -1472,3 +1481,6 @@ Qed.
  Qed.
 
 End MakeRingPol.
+
+Arguments PEO [C].
+Arguments PEI [C].
\ No newline at end of file
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 7a7ffcfdc5..1d958d09b2 100644
--- a/plugins/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
@@ -196,12 +196,17 @@ Ltac get_MonPol lemma :=
 (********************************************************)
 
 (* Building the atom list of a ring expression *)
-Ltac FV Cst CstPow add mul sub opp pow t fv :=
+(* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+(* the tactic could be used to discriminate occurrences of an opaque *)
+(* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac FV Cst CstPow rO rI add mul sub opp pow t fv :=
  let rec TFV t fv :=
   let f :=
   match Cst t with
   | NotConstant =>
       match t with
+      | rO =>  fun _ => fv
+      | rI =>  fun _ => fv
       | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
       | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
@@ -219,12 +224,19 @@ Ltac FV Cst CstPow add mul sub opp pow t fv :=
  in TFV t fv.
 
  (* syntaxification of ring expressions *)
-Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
+ (* We do not assume that Cst recognizes the rO and rI terms as constants, as *)
+ (* the tactic could be used to discriminate occurrences of an opaque *)
+ (* constant phi, with (phi 0) not convertible to 0 for instance *)
+Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv :=
  let rec mkP t :=
     let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with
+        | rO => 
+          fun _ => constr:(@PEO C)
+        | rI => 
+          fun _ => constr:(@PEI C)
         | (radd ?t1 ?t2) =>
           fun _ =>
           let e1 := mkP t1 in
@@ -260,58 +272,58 @@ Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post :=
   let RNG :=
     match type of lemma1 with
     | context
-       [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+       [@PEeval ?R ?r0 ?r1 ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
         (fun proj => proj
              cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2)
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2)
     | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
     end in
   F RNG.
 
 Ltac get_Carrier RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             R).
 
 Ltac get_Eq RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             req).
 
 Ltac get_Pre RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             pre).
 
 Ltac get_Post RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             post).
 
 Ltac get_NormLemma RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             lemma1).
 
 Ltac get_SimplifyLemma RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
             lemma2).
 
 Ltac get_RingFV RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-            FV cst_tac pow_tac add mul sub opp pow).
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            FV cst_tac pow_tac r0 r1 add mul sub opp pow).
 
 Ltac get_RingMeta RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-            mkPolexpr C cst_tac pow_tac add mul sub opp pow).
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow).
 
 Ltac get_RingHypTac RNG :=
   RNG ltac:(fun cst_tac pow_tac pre post
-             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
-       let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in
+             R req r0 r1 add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+       let mkPol := mkPolexpr C cst_tac pow_tac r0 r1 add mul sub opp pow in
        fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
 
 (* ring tactics *)
@@ -338,7 +350,7 @@ Ltac Ring RNG lemma lH :=
     (apply (lemma vfv vlpe pe1 pe2)
       || fail "typing error while applying ring");
     [ ((let prh := proofHyp_tac lH in exact prh)
-        || idtac "can not automatically proof hypothesis :";
+        || idtac "can not automatically prove hypothesis :";
            idtac " maybe a left member of a hypothesis is not a monomial")
     | vm_compute;
       (exact (eq_refl true) || fail "not a valid ring equation")]).
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 7e4fc72776..f618c54b00 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -599,26 +599,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
     | Some (Closed lc) ->
         closed_term_ast (List.map Smartlocate.global_with_alias lc)
     | None ->
-        (match rk, opp, kind with
-            Abstract, None, _ ->
-              let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morphN) in
-              TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul]))
-          | Abstract, Some opp, Some _ ->
-              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphZ) in
-              TacArg(Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp]))
-          | Abstract, Some opp, None ->
-              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morphNword) in
-              TacArg
-                (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;add;mul;opp]))
-          | Computational _,_,_ ->
-              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in
-              TacArg
-                (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;zero;one]))
-          | Morphism mth,_,_ ->
-              let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
-              let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_gen) in
-              TacArg
-                (Loc.ghost,TacCall(Loc.ghost,t,List.map carg [zero;one;czero;cone])))
+        let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
+              TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
 
 let make_hyp env c =
   let t = Retyping.get_type_of env Evd.empty c in
@@ -857,8 +839,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|13->Eval|12->Rec|_->Prot)]);;
-(*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
+     my_constant "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
+(*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
 
 
 let _ = Redexpr.declare_reduction "simpl_field_expr"