ring2, cring, nsatz avec type classe avec parametres plus notations

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

7 files changed, 740 insertions, 1010 deletions

diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
index 79f5393dd..5b566dbb0 100644
--- a/plugins/setoid_ring/Algebra_syntax.v
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -1,18 +1,49 @@
-Class Zero (A : Type) := {zero : A}.
+
+Class Zero (A : Type) := zero : A.
 Notation "0" := zero.
-Class One (A : Type) := {one : A}.
+Class One (A : Type) := one : A.
 Notation "1" := one.
-Class Addition (A : Type) := {addition : A -> A -> A}.
+Class Addition (A : Type) := addition : A -> A -> A.
+Notation "_+_" := addition.
 Notation "x + y" := (addition x y).
-Class Multiplication {A B : Type} := {multiplication : A -> B -> B}.
+Class Multiplication {A B : Type} := multiplication : A -> B -> B.
+Notation "_*_" := multiplication.
 Notation "x * y" := (multiplication x y).
-Class Subtraction (A : Type) := {subtraction : A -> A -> A}.
+Class Subtraction (A : Type) := subtraction : A -> A -> A.
+Notation "_-_" := subtraction.
 Notation "x - y" := (subtraction x y).
-Class Opposite (A : Type) := {opposite : A -> A}.
-Notation "- x" := (opposite x).
-Class Equality {A : Type}:= {equality : A -> A -> Prop}.
+Class Opposite (A : Type) := opposite : A -> A.
+Notation "-_" := opposite.
+Notation "- x" := (opposite(x)).
+Class Equality {A : Type}:= equality : A -> A -> Prop.
+Notation "_==_" := equality.
 Notation "x == y" := (equality x y) (at level 70, no associativity).
-Class Bracket (A B: Type):= {bracket : A -> B}.
-Notation "[ x ]" := (bracket x).
-Class Power {A B: Type} := {power : A -> B -> A}.
-Notation "x ^ y" := (power x y).
\ No newline at end of file
+Class Bracket (A B: Type):= bracket : A -> B.
+Notation "[ x ]" := (bracket(x)).
+Class Power {A B: Type} := power : A -> B -> A.
+Notation "x ^ y" := (power x y).
+
+
+Notation "\/ x y z ,  P" := (forall x y z, P)
+   (at level 200, x ident, y ident, z ident).
+Notation "\/ x y ,  P" := (forall x y, P)
+   (at level 200, x ident, y ident).
+Notation "\/ x , P" := (forall x, P)(at level 200, x ident).
+
+Notation "\/ x y z : T ,  P" := (forall x y z : T, P)
+   (at level 200, x ident, y ident, z ident).
+Notation "\/ x y  : T ,  P" := (forall x y : T, P)
+   (at level 200, x ident, y ident).
+Notation "\/ x  : T , P" := (forall x : T, P)(at level 200, x ident).
+
+Notation "\ x y z , P" := (fun x y z => P)
+   (at level 200, x ident, y ident, z ident).
+Notation "\ x y ,  P" := (fun x y => P)
+   (at level 200, x ident, y ident).
+Notation "\ x , P" := (fun x => P)(at level 200, x ident).
+
+Notation "\ x y z : T , P" := (fun x y z : T => P)
+   (at level 200, x ident, y ident, z ident).
+Notation "\ x y : T ,  P" := (fun x y : T => P)
+   (at level 200, x ident, y ident).
+Notation "\ x : T , P" := (fun x : T => P)(at level 200, x ident).
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 4058cd224..367958a6b 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -6,383 +6,122 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* non commutative rings *)
-
+Require Import List.
 Require Import Setoid.
 Require Import BinPos.
-Require Import BinNat.
-Require Export ZArith.
+Require Import BinList.
+Require Import Znumtheory.
+Require Import Zdiv_def.
 Require Export Morphisms Setoid Bool.
-Require Import Algebra_syntax.
-Require Import Ring_theory.
-
-Set Implicit Arguments.
-
-Class Cring (R:Type) := {
- cring0: R; cring1: R; 
- cring_plus: R->R->R; cring_mult: R->R->R;
- cring_sub:  R->R->R; cring_opp: R->R; 
- cring_eq : R -> R -> Prop;
- cring_setoid: Equivalence cring_eq;
- cring_plus_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_plus;
- cring_mult_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_mult;
- cring_sub_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_sub;
- cring_opp_comp: Proper (cring_eq==>cring_eq) cring_opp;
-
- cring_add_0_l    : forall x, cring_eq (cring_plus cring0 x) x;
- cring_add_comm    : forall x y, cring_eq (cring_plus x y) (cring_plus y x);
- cring_add_assoc  : forall x y z, cring_eq (cring_plus x (cring_plus y z))
-                                         (cring_plus (cring_plus x y) z);
- cring_mul_1_l    : forall x, cring_eq (cring_mult cring1 x) x;
- cring_mul_assoc  : forall x y z, cring_eq (cring_mult x (cring_mult y z))
-                                         (cring_mult (cring_mult x y) z);
- cring_mul_comm    : forall x y, cring_eq (cring_mult x y) (cring_mult y x);
- cring_distr_l    : forall x y z, cring_eq (cring_mult (cring_plus x y) z)
-                                   (cring_plus (cring_mult x z) (cring_mult y z));
- cring_sub_def    : forall x y, cring_eq (cring_sub x y) (cring_plus x (cring_opp y));
- cring_opp_def    : forall x, cring_eq (cring_plus x (cring_opp x)) cring0
-}.
-
-(* Syntax *)
-
-Instance zero_cring `{R:Type}`{Rr:Cring R} : Zero R := {zero := cring0}.
-Instance one_cring`{R:Type}`{Rr:Cring R} : One R := {one := cring1}.
-Instance addition_cring`{R:Type}`{Rr:Cring R} : Addition R :=
-  {addition x y := cring_plus x y}.
-Instance multiplication_cring`{R:Type}`{Rr:Cring R} : Multiplication:= 
-  {multiplication x y := cring_mult x y}.
-Instance subtraction_cring`{R:Type}`{Rr:Cring R} : Subtraction R :=
-  {subtraction x y := cring_sub x y}.
-Instance opposite_cring`{R:Type}`{Rr:Cring R} : Opposite R := 
-  {opposite x := cring_opp x}.
-Instance equality_cring `{R:Type}`{Rr:Cring R} : Equality :=
-  {equality x y := cring_eq x y}.
-Definition ZN(x:Z):=
-  match x with
-    Z0 => N0
-    |Zpos p | Zneg p => Npos p
-end.
-Instance power_cring {R:Type}{Rr:Cring R} : Power:=
-  {power x y := @Ring_theory.pow_N _ cring1 cring_mult x (ZN y)}.
-
-Existing Instance cring_setoid.
-Existing Instance cring_plus_comp.
-Existing Instance cring_mult_comp.
-Existing Instance cring_sub_comp.
-Existing Instance cring_opp_comp.
-(** Interpretation morphisms definition*)
-
-Class Cring_morphism (C R:Type)`{Cr:Cring C} `{Rr:Cring R}:= {
-    cring_morphism_fun: C -> R;
-    cring_morphism0    : cring_morphism_fun 0 == 0;
-    cring_morphism1    : cring_morphism_fun 1 == 1;
-    cring_morphism_add : forall x y, cring_morphism_fun (x + y)
-                     == cring_morphism_fun x + cring_morphism_fun y;
-    cring_morphism_sub : forall x y, cring_morphism_fun (x - y)
-                     == cring_morphism_fun x - cring_morphism_fun y;
-    cring_morphism_mul : forall x y, cring_morphism_fun (x * y)
-                     == cring_morphism_fun x * cring_morphism_fun y;
-    cring_morphism_opp : forall x, cring_morphism_fun (-x)
-                          == -(cring_morphism_fun x);
-    cring_morphism_eq  : forall x y, x == y
-       -> cring_morphism_fun x == cring_morphism_fun y}.
-
-Instance bracket_cring {C R:Type}`{Cr:Cring C} `{Rr:Cring R}
-   `{phi:@Cring_morphism C R Cr Rr}
-  : Bracket C R  :=
-  {bracket x := cring_morphism_fun x}.
-
-(* Tactics for crings *)
-
-Lemma cring_syntax1:forall (A:Type)(Ar:Cring A), (@cring_eq _ Ar) = equality.
-intros. symmetry. simpl ; reflexivity. Qed.
-Lemma cring_syntax2:forall (A:Type)(Ar:Cring A), (@cring_plus _ Ar) = addition.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma cring_syntax3:forall (A:Type)(Ar:Cring A), (@cring_mult _ Ar) = multiplication.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma cring_syntax4:forall (A:Type)(Ar:Cring A), (@cring_sub _ Ar) = subtraction.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma cring_syntax5:forall (A:Type)(Ar:Cring A), (@cring_opp _ Ar) = opposite.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma cring_syntax6:forall (A:Type)(Ar:Cring A), (@cring0 _ Ar) = zero.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma cring_syntax7:forall (A:Type)(Ar:Cring A), (@cring1 _ Ar) = one.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma cring_syntax8:forall (A:Type)(Ar:Cring A)(B:Type)(Br:Cring B)
-  (pM:@Cring_morphism A B Ar Br), (@cring_morphism_fun _ _ _ _ pM) = bracket.
-intros. symmetry. simpl; reflexivity. Qed.
-
-Ltac set_cring_notations :=
-  repeat (rewrite cring_syntax1);
-  repeat (rewrite cring_syntax2);
-  repeat (rewrite cring_syntax3);
-  repeat (rewrite cring_syntax4);
-  repeat (rewrite cring_syntax5);
-  repeat (rewrite cring_syntax6);
-  repeat (rewrite cring_syntax7);
-  repeat (rewrite cring_syntax8).
-
-Ltac unset_cring_notations :=
-  unfold equality, equality_cring, addition, addition_cring,
-     multiplication, multiplication_cring, subtraction, subtraction_cring,
-     opposite, opposite_cring, one, one_cring, zero, zero_cring,
-     bracket, bracket_cring, power, power_cring.
-
-Ltac cring_simpl := simpl; set_cring_notations.
-
-Ltac cring_rewrite H:=
-  generalize H;
-  let h := fresh "H" in
-  unset_cring_notations; intro h;
-  rewrite h; clear h;
-  set_cring_notations.
-
-Ltac cring_rewrite_rev H:=
-  generalize H;
-  let h := fresh "H" in
-  unset_cring_notations; intro h;
-  rewrite <- h; clear h;
-  set_cring_notations.
-
-Ltac rrefl := unset_cring_notations; reflexivity.
-
-(* Useful properties *)
-
-Section Cring.
-
-Variable R: Type.
-Variable Rr: Cring R.
-
-(* Powers *)
-
- Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
-  match i with
-  | xH => x
-  | xO i => let p := pow_pos x i in p * p
-  | xI i => let p := pow_pos x i in x * (p * p)
+Require Import ZArith.
+Require Export Algebra_syntax.
+Require Export Ring2.
+Require Export Ring2_initial.
+Require Export Ring2_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
+     nil => idtac
+   | ?e1::?e2::_ =>  
+        match goal with
+          |- (?op ?u1 ?u2) =>
+           change (op 
+             (@Ring_polynom.PEeval
+               _ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n)
+               (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
+             (@Ring_polynom.PEeval
+               _ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n)
+               (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
+        end
   end.
-Add Setoid R cring_eq cring_setoid as R_set_Power.
- Add Morphism cring_mult : rmul_ext_Power. exact cring_mult_comp. Qed.
-
- Lemma pow_pos_comm : forall x j,  x * pow_pos x j == pow_pos x j * x.
-induction j; cring_simpl. 
-cring_rewrite_rev cring_mul_assoc. cring_rewrite_rev cring_mul_assoc. 
-cring_rewrite_rev IHj. cring_rewrite (cring_mul_assoc (pow_pos x j) x (pow_pos x j)).
-cring_rewrite_rev IHj. cring_rewrite_rev cring_mul_assoc. rrefl.
-cring_rewrite_rev cring_mul_assoc. cring_rewrite_rev IHj.
-cring_rewrite cring_mul_assoc. cring_rewrite IHj.
-cring_rewrite_rev cring_mul_assoc. cring_rewrite IHj. rrefl. rrefl.
-Qed.
-
- Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
- Proof.
-  induction j; cring_simpl. 
-  cring_rewrite IHj. 
-cring_rewrite_rev (cring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
-cring_rewrite (cring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
-  cring_rewrite_rev pow_pos_comm. unset_cring_notations.
-rewrite <- cring_mul_assoc. reflexivity.
-rrefl. rrefl.
-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 cring_rewrite IHi.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
-  cring_rewrite pow_pos_Psucc.
-  cring_simpl;repeat cring_rewrite cring_mul_assoc. rrefl.
-  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat cring_rewrite IHi. cring_rewrite cring_mul_assoc. rrefl.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;cring_rewrite pow_pos_Psucc.
-   simpl. reflexivity. 
- Qed.
-
- Definition pow_N (x:R) (p:N) :=
-  match p with
-  | N0 => 1
-  | Npos p => pow_pos x p
+Section cring.
+Context {R:Type}`{Rr:Cring R}.
+
+Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
+intros. apply mk_reqe;intros. 
+rewrite H. rewrite H0. reflexivity.
+rewrite H. rewrite H0. reflexivity.
+ rewrite H. reflexivity. Defined.
+
+Lemma cring_almost_ring_theory:
+   almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
+intros. apply mk_art ;intros. 
+rewrite ring_add_0_l; reflexivity. 
+rewrite ring_add_comm; reflexivity. 
+rewrite ring_add_assoc; reflexivity. 
+rewrite ring_mul_1_l; reflexivity. 
+apply ring_mul_0_l.
+rewrite cring_mul_comm; reflexivity. 
+rewrite ring_mul_assoc; reflexivity. 
+rewrite ring_distr_l; reflexivity. 
+rewrite ring_opp_mul_l; reflexivity. 
+apply ring_opp_add.
+rewrite ring_sub_def ; reflexivity. Defined.
+
+Lemma cring_morph:
+  ring_morph  zero one _+_ _*_ _-_ -_ _==_
+             0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+             gen_phiZ.
+intros. apply mkmorph ; intros; simpl; try reflexivity.
+rewrite gen_phiZ_add; reflexivity.
+rewrite ring_sub_def. unfold Zminus. rewrite gen_phiZ_add.
+rewrite gen_phiZ_opp; reflexivity.
+rewrite gen_phiZ_mul; reflexivity.
+rewrite gen_phiZ_opp; reflexivity.
+rewrite (Zeqb_ok x y H). reflexivity. Defined.
+
+Lemma cring_power_theory : 
+  @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n)
+  (@Ring_theory.pow_N _  1 multiplication).
+intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
+
+Lemma cring_div_theory: 
+  div_theory _==_ Zplus Zmult gen_phiZ Zquotrem.
+intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
+simpl.   apply ring_setoid. Defined.
+End cring.
+
+Ltac cring_gen :=
+  match goal with
+    |- ?g => let lterm := lterm_goal g in (* les variables *)
+        match eval red in (list_reifyl (lterm:=lterm)) with
+          | (?fv, ?lexpr) => 
+           (*idtac "variables:";idtac fv;
+           idtac "terms:"; idtac lterm;
+           idtac "reifications:"; idtac lexpr; *)
+           reify_goal fv lexpr lterm;
+           match goal with 
+             |- ?g => 
+               generalize
+                 (@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_
+                        ring_setoid
+                        cring_eq_ext
+                        cring_almost_ring_theory
+                        Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+                        gen_phiZ
+                        cring_morph
+                        N
+                        (fun n:N => n)
+                        (@Ring_theory.pow_N _  1 multiplication)
+                        cring_power_theory
+                        Zquotrem
+                        cring_div_theory
+                        O fv nil);
+                 let rc := fresh "rc"in
+                   intro rc; apply rc
+           end
+        end
   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; rrefl.
- Qed.
-
-End Cring.
-
-
-
-
-Section Cring2.
-Variable R: Type.
-Variable Rr: Cring R.
- (** Identity is a morphism *)
- Definition IDphi (x:R) := x.
- Lemma IDmorph : @Cring_morphism R R Rr Rr.
- Proof.
-  apply (Build_Cring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial.
- Qed.
-
-Ltac cring_replace a b :=
-  unset_cring_notations; setoid_replace a with b; set_cring_notations.
-
- (** crings are almost crings*)
- Lemma cring_mul_0_l : forall x, 0 * x == 0.
- Proof.
-  intro x. cring_replace (0*x) ((0+1)*x + -x). 
-  cring_rewrite cring_add_0_l. cring_rewrite cring_mul_1_l .
-  cring_rewrite cring_opp_def ;rrefl.
-  cring_rewrite cring_distr_l ;cring_rewrite cring_mul_1_l .
-  cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def .
-  cring_rewrite cring_add_comm ; cring_rewrite cring_add_0_l ;rrefl.
- Qed.
-
-Lemma cring_mul_1_r: forall x, x * 1 == x.
-intro x. cring_rewrite (cring_mul_comm x 1). cring_rewrite cring_mul_1_l.
-rrefl. Qed.
-
-Lemma cring_distr_r: forall x y z,
-  x*(y+z) == x*y + x*z.
-intros. cring_rewrite (cring_mul_comm x (y+z)).
-cring_rewrite cring_distr_l. cring_rewrite (cring_mul_comm x y).
- cring_rewrite (cring_mul_comm x z). rrefl. Qed.
-
- Lemma cring_mul_0_r : forall x, x * 0 == 0.
- Proof.
-  intro x; cring_replace (x*0)  (x*(0+1) + -x).
-  cring_rewrite cring_add_0_l ;  cring_rewrite cring_mul_1_r .
-  cring_rewrite cring_opp_def ;rrefl.
-  cring_rewrite cring_distr_r . cring_rewrite cring_mul_1_r .
-  cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def .
-  cring_rewrite cring_add_comm ; cring_rewrite cring_add_0_l ;rrefl.
- Qed.
-
- Lemma cring_opp_mul_l : forall x y, -(x * y) == -x * y.
- Proof.
-  intros x y;cring_rewrite_rev (cring_add_0_l (- x * y)).
-  cring_rewrite cring_add_comm .
-  cring_rewrite_rev (cring_opp_def (x*y)).
-  cring_rewrite cring_add_assoc .
-  cring_rewrite_rev cring_distr_l.
-  cring_rewrite (cring_add_comm (-x));cring_rewrite cring_opp_def .
-  cring_rewrite cring_mul_0_l;cring_rewrite cring_add_0_l ;rrefl.
- Qed.
-
-Lemma cring_opp_mul_r : forall x y, -(x * y) == x * -y.
- Proof.
-  intros x y;cring_rewrite_rev (cring_add_0_l (x * - y)).
-  cring_rewrite cring_add_comm .
-  cring_rewrite_rev (cring_opp_def (x*y)).
-  cring_rewrite cring_add_assoc .
-  cring_rewrite_rev cring_distr_r .
-  cring_rewrite (cring_add_comm (-y));cring_rewrite cring_opp_def .
-  cring_rewrite cring_mul_0_r;cring_rewrite cring_add_0_l ;rrefl.
- Qed.
-
- Lemma cring_opp_add : forall x y, -(x + y) == -x + -y.
- Proof.
-  intros x y;cring_rewrite_rev (cring_add_0_l  (-(x+y))).
-  cring_rewrite_rev (cring_opp_def  x).
-  cring_rewrite_rev (cring_add_0_l  (x + - x + - (x + y))).
-  cring_rewrite_rev (cring_opp_def  y).
-  cring_rewrite (cring_add_comm  x).
-  cring_rewrite (cring_add_comm  y).
-  cring_rewrite_rev (cring_add_assoc  (-y)).
-  cring_rewrite_rev (cring_add_assoc  (- x)).
-  cring_rewrite (cring_add_assoc   y).
-  cring_rewrite (cring_add_comm  y).
-  cring_rewrite_rev (cring_add_assoc   (- x)).
-  cring_rewrite (cring_add_assoc  y).
-  cring_rewrite (cring_add_comm  y);cring_rewrite cring_opp_def .
-  cring_rewrite (cring_add_comm  (-x) 0);cring_rewrite cring_add_0_l .
-  cring_rewrite cring_add_comm; rrefl.
- Qed.
-
- Lemma cring_opp_opp : forall x, - -x == x.
- Proof.
-  intros x; cring_rewrite_rev (cring_add_0_l (- -x)).
-  cring_rewrite_rev (cring_opp_def x).
-  cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def .
-  cring_rewrite (cring_add_comm  x); cring_rewrite cring_add_0_l . rrefl.
- Qed.
-
- Lemma cring_sub_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
- Proof.
-  intros.
-  cring_replace (x1 - y1)  (x1 + -y1).
-  cring_replace (x2 - y2)  (x2 + -y2).
-  cring_rewrite H;cring_rewrite H0;rrefl.
-  cring_rewrite cring_sub_def. rrefl.
-  cring_rewrite cring_sub_def. rrefl.
- Qed.
-
- Ltac mcring_rewrite :=
-   repeat first
-     [ cring_rewrite cring_add_0_l
-     | cring_rewrite_rev (cring_add_comm 0)
-     | cring_rewrite cring_mul_1_l
-     | cring_rewrite cring_mul_0_l
-     | cring_rewrite cring_distr_l
-     | rrefl
-     ].
-
- Lemma cring_add_0_r : forall x, (x + 0) == x.
- Proof. intros; mcring_rewrite. Qed.
-
- 
- Lemma cring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
- Proof.
-  intros;cring_rewrite_rev (cring_add_assoc x).
-  cring_rewrite (cring_add_comm x);rrefl.
- Qed.
-
- Lemma cring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
- Proof.
-  intros; repeat cring_rewrite_rev cring_add_assoc.
-   cring_rewrite (cring_add_comm x); rrefl.
- Qed.
-
- Lemma cring_opp_zero : -0 == 0.
- Proof.
-  cring_rewrite_rev (cring_mul_0_r 0). cring_rewrite cring_opp_mul_l.
-  repeat cring_rewrite cring_mul_0_r. rrefl.
- Qed.
-
-End Cring2.
+Ltac cring_compute:= vm_compute; reflexivity.
 
-(** Some simplification tactics*)
-Ltac gen_reflexivity := rrefl.
- 
-Ltac gen_cring_rewrite :=
-  repeat first
-     [ rrefl
-     | progress cring_rewrite cring_opp_zero
-     | cring_rewrite cring_add_0_l
-     | cring_rewrite cring_add_0_r
-     | cring_rewrite cring_mul_1_l 
-     | cring_rewrite cring_mul_1_r
-     | cring_rewrite cring_mul_0_l 
-     | cring_rewrite cring_mul_0_r 
-     | cring_rewrite cring_distr_l 
-     | cring_rewrite cring_distr_r 
-     | cring_rewrite cring_add_assoc 
-     | cring_rewrite cring_mul_assoc
-     | progress cring_rewrite cring_opp_add 
-     | progress cring_rewrite cring_sub_def 
-     | progress cring_rewrite_rev cring_opp_mul_l 
-     | progress cring_rewrite_rev cring_opp_mul_r ].
+Ltac cring:= 
+  intros;
+  cring_gen;
+  cring_compute.
 
-Ltac gen_add_push x :=
-set_cring_notations;
-repeat (match goal with
-  | |- context [(?y + x) + ?z] =>
-     progress cring_rewrite (@cring_add_assoc2 _ _ x y z)
-  | |- context [(x + ?y) + ?z] =>
-     progress cring_rewrite  (@cring_add_assoc1 _ _ x y z)
-  end).
diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ring2.v
index a28c1d4ea..bf65e8384 100644
--- a/plugins/setoid_ring/Ring2.v
+++ b/plugins/setoid_ring/Ring2.v
@@ -12,138 +12,59 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import BinNat.
 Require Export Morphisms Setoid Bool.
+Require Export ZArith.
 Require Export Algebra_syntax.
 
 Set Implicit Arguments.
 
-Class Ring (R:Type) := {
- ring0: R; ring1: R; 
- ring_plus: R->R->R; ring_mult: R->R->R;
- ring_sub:  R->R->R; ring_opp: R->R; 
- ring_eq : R -> R -> Prop;
- ring_setoid: Equivalence ring_eq;
- ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus;
- ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult;
- ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub;
- ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp;
-
- ring_add_0_l    : forall x, ring_eq (ring_plus ring0 x) x;
- ring_add_comm    : forall x y, ring_eq (ring_plus x y) (ring_plus y x);
- ring_add_assoc  : forall x y z, ring_eq (ring_plus x (ring_plus y z))
-                                         (ring_plus (ring_plus x y) z);
- ring_mul_1_l    : forall x, ring_eq (ring_mult ring1 x) x;
- ring_mul_1_r    : forall x, ring_eq (ring_mult x ring1) x;
- ring_mul_assoc  : forall x y z, ring_eq (ring_mult x (ring_mult y z))
-                                         (ring_mult (ring_mult x y) z);
- ring_distr_l    : forall x y z, ring_eq (ring_mult (ring_plus x y) z)
-                                   (ring_plus (ring_mult x z) (ring_mult y z));
- ring_distr_r    : forall x y z, ring_eq (ring_mult z (ring_plus x y))
-                                  (ring_plus (ring_mult z x) (ring_mult z y));
- ring_sub_def    : forall x y, ring_eq (ring_sub x y) (ring_plus x (ring_opp y));
- ring_opp_def    : forall x, ring_eq (ring_plus x (ring_opp x)) ring0
+Class Ring_ops(T:Type)
+   {ring0:T}
+   {ring1:T}
+   {add:T->T->T}
+   {mul:T->T->T}
+   {sub:T->T->T}
+   {opp:T->T}
+   {ring_eq:T->T->Prop}.
+
+Instance zero_notation(T:Type)`{Ring_ops T}:Zero T. exact ring0. Defined.
+Instance one_notation(T:Type)`{Ring_ops T}:One T. exact ring1. Defined.
+Instance add_notation(T:Type)`{Ring_ops T}:Addition T. exact add. Defined.
+Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T.
+     exact mul. Defined.
+Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T. exact sub. Defined.
+Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T. exact opp. Defined.
+Instance eq_notation(T:Type)`{Ring_ops T}:@Equality T. exact ring_eq. Defined.
+
+Class Ring `{Ro:Ring_ops}:={
+ ring_setoid: Equivalence _==_;
+ ring_plus_comp: Proper (_==_ ==> _==_ ==>_==_) _+_;
+ ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_;
+ ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_;
+ ring_opp_comp: Proper (_==_==>_==_) -_;
+ ring_add_0_l    : \/x, 0 + x == x;
+ ring_add_comm   : \/x y, x + y == y + x;
+ ring_add_assoc  : \/x y z, x + (y + z) == (x + y) + z;
+ ring_mul_1_l    : \/x, 1 * x == x;
+ ring_mul_1_r    : \/x, x * 1 == x;
+ ring_mul_assoc  : \/x y z, x * (y * z) == (x * y) * z;
+ ring_distr_l    : \/x y z, (x + y) * z == x * z + y * z;
+ ring_distr_r    : \/x y z, z * ( x + y) == z * x + z * y;
+ ring_sub_def    : \/x y, x - y == x + -y;
+ ring_opp_def    : \/x, x + -x == 0
 }.
 
-
-Instance zero_ring (R:Type)(Rr:Ring R) : Zero R := {zero := ring0}.
-Instance one_ring(R:Type)(Rr:Ring R) : One R := {one := ring1}.
-Instance addition_ring(R:Type)(Rr:Ring R) : Addition R :=
-  {addition x y := ring_plus x y}.
-Instance multiplication_ring(R:Type)(Rr:Ring R) : Multiplication:= 
-  {multiplication x y := ring_mult x y}.
-Instance subtraction_ring(R:Type)(Rr:Ring R) : Subtraction R :=
-  {subtraction x y := ring_sub x y}.
-Instance opposite_ring(R:Type)(Rr:Ring R) : Opposite R := 
-  {opposite x := ring_opp x}.
-Instance equality_ring(R:Type)(Rr:Ring R) : Equality :=
-  {equality x y := ring_eq x y}.
+Instance ring_Ring_ops(R:Type)`{Ring R}
+  :@Ring_ops R 0 1 addition multiplication subtraction opposite equality.
 
 Existing Instance ring_setoid.
 Existing Instance ring_plus_comp.
 Existing Instance ring_mult_comp.
 Existing Instance ring_sub_comp.
 Existing Instance ring_opp_comp.
-(** Interpretation morphisms definition*)
-
-Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}:= {
-    ring_morphism_fun: C -> R;
-    ring_morphism0    : ring_morphism_fun 0 == 0;
-    ring_morphism1    : ring_morphism_fun 1 == 1;
-    ring_morphism_add : forall x y, ring_morphism_fun (x + y)
-                     == ring_morphism_fun x + ring_morphism_fun y;
-    ring_morphism_sub : forall x y, ring_morphism_fun (x - y)
-                     == ring_morphism_fun x - ring_morphism_fun y;
-    ring_morphism_mul : forall x y, ring_morphism_fun (x * y)
-                     == ring_morphism_fun x * ring_morphism_fun y;
-    ring_morphism_opp : forall x, ring_morphism_fun (-x)
-                          == -(ring_morphism_fun x);
-    ring_morphism_eq  : forall x y, x == y
-       -> ring_morphism_fun x == ring_morphism_fun y}.
-
-Instance bracket_ring (C R:Type)`{Cr:Ring C} `{Rr:Ring R}
-   `{phi:@Ring_morphism C R Cr Rr}
-  : Bracket C R  :=
-  {bracket x := ring_morphism_fun x}.
-
-(* Tactics for rings *)
-
-Lemma ring_syntax1:forall (A:Type)(Ar:Ring A), (@ring_eq _ Ar) = equality.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax2:forall (A:Type)(Ar:Ring A), (@ring_plus _ Ar) = addition.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax3:forall (A:Type)(Ar:Ring A), (@ring_mult _ Ar) = multiplication.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax4:forall (A:Type)(Ar:Ring A), (@ring_sub _ Ar) = subtraction.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax5:forall (A:Type)(Ar:Ring A), (@ring_opp _ Ar) = opposite.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax6:forall (A:Type)(Ar:Ring A), (@ring0 _ Ar) = zero.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax7:forall (A:Type)(Ar:Ring A), (@ring1 _ Ar) = one.
-intros. symmetry. simpl; reflexivity. Qed.
-Lemma ring_syntax8:forall (A:Type)(Ar:Ring A)(B:Type)(Br:Ring B)
-  (pM:@Ring_morphism A B Ar Br), (@ring_morphism_fun _ _ _ _ pM) = bracket.
-intros. symmetry. simpl; reflexivity. Qed.
-
-Ltac set_ring_notations :=
-  repeat (rewrite ring_syntax1);
-  repeat (rewrite ring_syntax2);
-  repeat (rewrite ring_syntax3);
-  repeat (rewrite ring_syntax4);
-  repeat (rewrite ring_syntax5);
-  repeat (rewrite ring_syntax6);
-  repeat (rewrite ring_syntax7);
-  repeat (rewrite ring_syntax8).
-
-Ltac unset_ring_notations :=
-  unfold equality, equality_ring, addition, addition_ring,
-     multiplication, multiplication_ring, subtraction, subtraction_ring,
-     opposite, opposite_ring, one, one_ring, zero, zero_ring,
-     bracket, bracket_ring.
-
-Ltac ring_simpl := simpl; set_ring_notations.
-
-Ltac ring_rewrite H:=
-  generalize H;
-  let h := fresh "H" in
-  unset_ring_notations; intro h;
-  rewrite h; clear h;
-  set_ring_notations.
-
-Ltac ring_rewrite_rev H:=
-  generalize H;
-  let h := fresh "H" in
-  unset_ring_notations; intro h;
-  rewrite <- h; clear h;
-  set_ring_notations.
-
-Ltac rrefl := unset_ring_notations; reflexivity.
-
-Section Ring.
 
-Variable R: Type.
-Variable Rr: Ring R.
+Section Ring_power.
 
-(* Powers *)
+Context {R:Type}`{Ring R}.
 
  Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
   match i with
@@ -151,219 +72,235 @@ Variable Rr: Ring R.
   | xO i => let p := pow_pos x i in p * p
   | xI i => let p := pow_pos x i in x * (p * p)
   end.
-Add Setoid R ring_eq ring_setoid as R_set_Power.
- Add Morphism ring_mult : rmul_ext_Power. exact ring_mult_comp. Qed.
-
- Lemma pow_pos_comm : forall x j,  x * pow_pos x j == pow_pos x j * x.
-induction j; ring_simpl. 
-ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev ring_mul_assoc. 
-ring_rewrite_rev IHj. ring_rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
-ring_rewrite_rev IHj. ring_rewrite_rev ring_mul_assoc. rrefl.
-ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev IHj.
-ring_rewrite ring_mul_assoc. ring_rewrite IHj.
-ring_rewrite_rev ring_mul_assoc. ring_rewrite IHj. rrefl. rrefl.
+
+ Definition pow_N (x:R) (p:N) :=
+  match p with
+  | N0 => 1
+  | Npos p => pow_pos x p
+  end.
+
+End Ring_power.
+
+Definition ZN(x:Z):=
+  match x with
+    Z0 => N0
+    |Zpos p | Zneg p => Npos p
+end.
+
+Instance power_ring {R:Type}`{Ring R} : Power:=
+  {power x y := pow_N x (ZN y)}.
+
+(** Interpretation morphisms definition*)
+
+Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= {
+    ring_morphism0    : [0] == 0;
+    ring_morphism1    : [1] == 1;
+    ring_morphism_add : \/x y, [x + y] == [x] + [y];
+    ring_morphism_sub : \/x y, [x - y] == [x] - [y];
+    ring_morphism_mul : \/x y, [x * y] == [x] * [y];
+    ring_morphism_opp : \/ x, [-x] == -[x];
+    ring_morphism_eq  : \/x y, x == y -> [x] == [y]}.
+
+Section Ring.
+
+Context {R:Type}`{Rr:Ring R}.
+
+(* Powers *)
+
+ Lemma pow_pos_comm : \/ x j,  x * pow_pos x j == pow_pos x j * x.
+induction j; simpl. rewrite <- ring_mul_assoc.
+rewrite <- ring_mul_assoc. 
+rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
+rewrite <- IHj. rewrite <- ring_mul_assoc. reflexivity.
+rewrite <- ring_mul_assoc. rewrite <- IHj.
+rewrite ring_mul_assoc. rewrite IHj.
+rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity.
 Qed.
 
- Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Lemma pow_pos_Psucc : \/ x j, pow_pos x (Psucc j) == x * pow_pos x j.
  Proof.
-  induction j; ring_simpl. 
-  ring_rewrite IHj. 
-ring_rewrite_rev (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
-ring_rewrite (ring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
-  ring_rewrite_rev pow_pos_comm. unset_ring_notations.
+  induction j; simpl. 
+  rewrite IHj. 
+rewrite <- (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
+rewrite (ring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
+  rewrite <- pow_pos_comm.
 rewrite <- ring_mul_assoc. reflexivity.
-rrefl. rrefl.
+reflexivity. reflexivity.
 Qed.
 
- Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Lemma pow_pos_Pplus : \/ 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 ring_rewrite IHi.
+  repeat rewrite IHi.
   rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
-  ring_rewrite pow_pos_Psucc.
-  ring_simpl;repeat ring_rewrite ring_mul_assoc. rrefl.
+  rewrite pow_pos_Psucc.
+  simpl;repeat rewrite ring_mul_assoc. reflexivity.
   rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
-  repeat ring_rewrite IHi. ring_rewrite ring_mul_assoc. rrefl.
-  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;ring_rewrite pow_pos_Psucc.
+  repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc.
    simpl. reflexivity. 
  Qed.
 
- Definition pow_N (x:R) (p:N) :=
-  match p with
-  | N0 => 1
-  | 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.
+ Lemma pow_N_pow_N : \/ x n, pow_N x (id_phi_N n) == pow_N x n.
  Proof.
-  intros; rrefl.
+  intros; reflexivity.
  Qed.
 
-End Ring.
-
-
-
-
-Section Ring2.
-Variable R: Type.
-Variable Rr: Ring R.
  (** Identity is a morphism *)
- Definition IDphi (x:R) := x.
- Lemma IDmorph : @Ring_morphism R R Rr Rr.
+ (*
+ Instance IDmorph : Ring_morphism _ _ _  (fun x => x).
  Proof.
-  apply (Build_Ring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial.
+  apply (Build_Ring_morphism H6 H6 (fun x => x));intros;
+  try reflexivity. trivial.
  Qed.
-
-Ltac ring_replace a b :=
-  unset_ring_notations; setoid_replace a with b; set_ring_notations.
-
+*)
  (** rings are almost rings*)
- Lemma ring_mul_0_l : forall x, 0 * x == 0.
+ Lemma ring_mul_0_l : \/ x, 0 * x == 0.
  Proof.
-  intro x. ring_replace (0*x) ((0+1)*x + -x). 
-  ring_rewrite ring_add_0_l. ring_rewrite ring_mul_1_l .
-  ring_rewrite ring_opp_def ;rrefl.
-  ring_rewrite ring_distr_l ;ring_rewrite ring_mul_1_l .
-  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
-  ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl.
+  intro x. setoid_replace (0*x) with ((0+1)*x + -x). 
+  rewrite ring_add_0_l. rewrite ring_mul_1_l .
+  rewrite ring_opp_def . fold zero. reflexivity.
+  rewrite ring_distr_l . rewrite ring_mul_1_l .
+  rewrite <- ring_add_assoc ; rewrite ring_opp_def .
+  rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity.
  Qed.
 
- Lemma ring_mul_0_r : forall x, x * 0 == 0.
+ Lemma ring_mul_0_r : \/ x, x * 0 == 0.
  Proof.
-  intro x; ring_replace (x*0)  (x*(0+1) + -x).
-  ring_rewrite ring_add_0_l ; ring_rewrite ring_mul_1_r .
-  ring_rewrite ring_opp_def ;rrefl.
+  intro x; setoid_replace (x*0)  with (x*(0+1) + -x).
+  rewrite ring_add_0_l ; rewrite ring_mul_1_r .
+  rewrite ring_opp_def ; fold zero; reflexivity.
 
-  ring_rewrite ring_distr_r ;ring_rewrite ring_mul_1_r .
-  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
-  ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl.
+  rewrite ring_distr_r ;rewrite ring_mul_1_r .
+  rewrite <- ring_add_assoc ; rewrite ring_opp_def .
+  rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity.
  Qed.
 
- Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y.
+ Lemma ring_opp_mul_l : \/x y, -(x * y) == -x * y.
  Proof.
-  intros x y;ring_rewrite_rev (ring_add_0_l (- x * y)).
-  ring_rewrite ring_add_comm .
-  ring_rewrite_rev (ring_opp_def (x*y)).
-  ring_rewrite ring_add_assoc .
-  ring_rewrite_rev ring_distr_l.
-  ring_rewrite (ring_add_comm (-x));ring_rewrite ring_opp_def .
-  ring_rewrite ring_mul_0_l;ring_rewrite ring_add_0_l ;rrefl.
+  intros x y;rewrite <- (ring_add_0_l (- x * y)).
+  rewrite ring_add_comm .
+  rewrite <- (ring_opp_def (x*y)).
+  rewrite ring_add_assoc .
+  rewrite <- ring_distr_l.
+  rewrite (ring_add_comm (-x));rewrite ring_opp_def .
+  rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity.
  Qed.
 
-Lemma ring_opp_mul_r : forall x y, -(x * y) == x * -y.
+Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y.
  Proof.
-  intros x y;ring_rewrite_rev (ring_add_0_l (x * - y)).
-  ring_rewrite ring_add_comm .
-  ring_rewrite_rev (ring_opp_def (x*y)).
-  ring_rewrite ring_add_assoc .
-  ring_rewrite_rev ring_distr_r .
-  ring_rewrite (ring_add_comm (-y));ring_rewrite ring_opp_def .
-  ring_rewrite ring_mul_0_r;ring_rewrite ring_add_0_l ;rrefl.
+  intros x y;rewrite <- (ring_add_0_l (x * - y)).
+  rewrite ring_add_comm .
+  rewrite <- (ring_opp_def (x*y)).
+  rewrite ring_add_assoc .
+  rewrite <- ring_distr_r .
+  rewrite (ring_add_comm (-y));rewrite ring_opp_def .
+  rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity.
  Qed.
 
- Lemma ring_opp_add : forall x y, -(x + y) == -x + -y.
+ Lemma ring_opp_add : \/x y, -(x + y) == -x + -y.
  Proof.
-  intros x y;ring_rewrite_rev (ring_add_0_l  (-(x+y))).
-  ring_rewrite_rev (ring_opp_def  x).
-  ring_rewrite_rev (ring_add_0_l  (x + - x + - (x + y))).
-  ring_rewrite_rev (ring_opp_def  y).
-  ring_rewrite (ring_add_comm  x).
-  ring_rewrite (ring_add_comm  y).
-  ring_rewrite_rev (ring_add_assoc  (-y)).
-  ring_rewrite_rev (ring_add_assoc  (- x)).
-  ring_rewrite (ring_add_assoc   y).
-  ring_rewrite (ring_add_comm  y).
-  ring_rewrite_rev (ring_add_assoc   (- x)).
-  ring_rewrite (ring_add_assoc  y).
-  ring_rewrite (ring_add_comm  y);ring_rewrite ring_opp_def .
-  ring_rewrite (ring_add_comm  (-x) 0);ring_rewrite ring_add_0_l .
-  ring_rewrite ring_add_comm; rrefl.
+  intros x y;rewrite <- (ring_add_0_l  (-(x+y))).
+  rewrite <- (ring_opp_def  x).
+  rewrite <- (ring_add_0_l  (x + - x + - (x + y))).
+  rewrite <- (ring_opp_def  y).
+  rewrite (ring_add_comm  x).
+  rewrite (ring_add_comm  y).
+  rewrite <- (ring_add_assoc  (-y)).
+  rewrite <- (ring_add_assoc  (- x)).
+  rewrite (ring_add_assoc   y).
+  rewrite (ring_add_comm  y).
+  rewrite <- (ring_add_assoc   (- x)).
+  rewrite (ring_add_assoc  y).
+  rewrite (ring_add_comm  y);rewrite ring_opp_def .
+  rewrite (ring_add_comm  (-x) 0);rewrite ring_add_0_l .
+  rewrite ring_add_comm; reflexivity.
  Qed.
 
- Lemma ring_opp_opp : forall x, - -x == x.
+ Lemma ring_opp_opp : \/ x, - -x == x.
  Proof.
-  intros x; ring_rewrite_rev (ring_add_0_l (- -x)).
-  ring_rewrite_rev (ring_opp_def x).
-  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
-  ring_rewrite (ring_add_comm  x); ring_rewrite ring_add_0_l . rrefl.
+  intros x; rewrite <- (ring_add_0_l (- -x)).
+  rewrite <- (ring_opp_def x).
+  rewrite <- ring_add_assoc ; rewrite ring_opp_def .
+  rewrite (ring_add_comm  x); rewrite ring_add_0_l . reflexivity.
  Qed.
 
  Lemma ring_sub_ext :
-      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+      \/ x1 x2, x1 == x2 -> \/ y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
  Proof.
   intros.
-  ring_replace (x1 - y1)  (x1 + -y1).
-  ring_replace (x2 - y2)  (x2 + -y2).
-  ring_rewrite H;ring_rewrite H0;rrefl.
-  ring_rewrite ring_sub_def. rrefl.
-  ring_rewrite ring_sub_def. rrefl.
+  setoid_replace (x1 - y1)  with (x1 + -y1).
+  setoid_replace (x2 - y2)  with (x2 + -y2).
+  rewrite H;rewrite H0;reflexivity.
+  rewrite ring_sub_def. reflexivity.
+  rewrite ring_sub_def. reflexivity.
  Qed.
 
- Ltac mring_rewrite :=
+ Ltac mrewrite :=
    repeat first
-     [ ring_rewrite ring_add_0_l
-     | ring_rewrite_rev (ring_add_comm 0)
-     | ring_rewrite ring_mul_1_l
-     | ring_rewrite ring_mul_0_l
-     | ring_rewrite ring_distr_l
-     | rrefl
+     [ rewrite ring_add_0_l
+     | rewrite <- (ring_add_comm 0)
+     | rewrite ring_mul_1_l
+     | rewrite ring_mul_0_l
+     | rewrite ring_distr_l
+     | reflexivity
      ].
 
- Lemma ring_add_0_r : forall x, (x + 0) == x.
- Proof. intros; mring_rewrite. Qed.
+ Lemma ring_add_0_r : \/ x, (x + 0) == x.
+ Proof. intros; mrewrite. Qed.
 
  
- Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Lemma ring_add_assoc1 : \/x y z, (x + y) + z == (y + z) + x.
  Proof.
-  intros;ring_rewrite_rev (ring_add_assoc x).
-  ring_rewrite (ring_add_comm x);rrefl.
+  intros;rewrite <- (ring_add_assoc x).
+  rewrite (ring_add_comm x);reflexivity.
  Qed.
 
- Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
+ Lemma ring_add_assoc2 : \/x y z, (y + x) + z == (y + z) + x.
  Proof.
-  intros; repeat ring_rewrite_rev ring_add_assoc.
-   ring_rewrite (ring_add_comm x); rrefl.
+  intros; repeat rewrite <- ring_add_assoc.
+   rewrite (ring_add_comm x); reflexivity.
  Qed.
 
  Lemma ring_opp_zero : -0 == 0.
  Proof.
-  ring_rewrite_rev (ring_mul_0_r 0). ring_rewrite ring_opp_mul_l.
-  repeat ring_rewrite ring_mul_0_r. rrefl.
+  rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l.
+  repeat rewrite ring_mul_0_r. reflexivity.
  Qed.
 
-End Ring2.
+End Ring.
 
 (** Some simplification tactics*)
-Ltac gen_reflexivity := rrefl.
+Ltac gen_reflexivity := reflexivity.
  
-Ltac gen_ring_rewrite :=
+Ltac gen_rewrite :=
   repeat first
-     [ rrefl
-     | progress ring_rewrite ring_opp_zero
-     | ring_rewrite ring_add_0_l
-     | ring_rewrite ring_add_0_r
-     | ring_rewrite ring_mul_1_l 
-     | ring_rewrite ring_mul_1_r
-     | ring_rewrite ring_mul_0_l 
-     | ring_rewrite ring_mul_0_r 
-     | ring_rewrite ring_distr_l 
-     | ring_rewrite ring_distr_r 
-     | ring_rewrite ring_add_assoc 
-     | ring_rewrite ring_mul_assoc
-     | progress ring_rewrite ring_opp_add 
-     | progress ring_rewrite ring_sub_def 
-     | progress ring_rewrite_rev ring_opp_mul_l 
-     | progress ring_rewrite_rev ring_opp_mul_r ].
+     [ reflexivity
+     | progress rewrite ring_opp_zero
+     | rewrite ring_add_0_l
+     | rewrite ring_add_0_r
+     | rewrite ring_mul_1_l 
+     | rewrite ring_mul_1_r
+     | rewrite ring_mul_0_l 
+     | rewrite ring_mul_0_r 
+     | rewrite ring_distr_l 
+     | rewrite ring_distr_r 
+     | rewrite ring_add_assoc 
+     | rewrite ring_mul_assoc
+     | progress rewrite ring_opp_add 
+     | progress rewrite ring_sub_def 
+     | progress rewrite <- ring_opp_mul_l 
+     | progress rewrite <- ring_opp_mul_r ].
 
 Ltac gen_add_push x :=
-set_ring_notations;
 repeat (match goal with
   | |- context [(?y + x) + ?z] =>
-     progress ring_rewrite (@ring_add_assoc2 _ _ x y z)
+     progress rewrite (ring_add_assoc2 x y z)
   | |- context [(x + ?y) + ?z] =>
-     progress ring_rewrite  (@ring_add_assoc1 _ _ x y z)
+     progress rewrite  (ring_add_assoc1 x y z)
   end).
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v
index 7c5631d4e..21b86ff37 100644
--- a/plugins/setoid_ring/Ring2_initial.v
+++ b/plugins/setoid_ring/Ring2_initial.v
@@ -10,7 +10,11 @@ Require Import ZArith_base.
 Require Import Zpow_def.
 Require Import BinInt.
 Require Import BinNat.
-Require Import Ndiv_def Zdiv_def.
+Require Import Setoid.
+Require Import BinList.
+Require Import BinPos.
+Require Import BinNat.
+Require Import BinInt.
 Require Import Setoid.
 Require Export Ring2.
 Require Export Ring2_polynom.
@@ -27,27 +31,26 @@ Lemma Zsth : Setoid_Theory Z (@eq Z).
 constructor;red;intros;subst;trivial.
 Qed.
 
-Definition Zr : Ring Z.
-apply (@Build_Ring Z Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z)); 
-try apply Zsth; try (red; red; intros; rewrite H; reflexivity). 
+Instance Zops:@Ring_ops Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z).
+
+Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops).
+constructor;
+try (try apply Zsth;
+   try (unfold respectful, Proper; unfold equality; unfold eq_notation in *;
+  intros; try rewrite H; try rewrite H0; reflexivity)).
  exact Zplus_comm. exact Zplus_assoc.
  exact Zmult_1_l.  exact Zmult_1_r. exact Zmult_assoc.
- exact Zmult_plus_distr_l.  intros; apply Zmult_plus_distr_r. trivial. exact Zminus_diag.
+ exact Zmult_plus_distr_l.  intros; apply Zmult_plus_distr_r.  exact Zminus_diag.
 Defined.
 
+(*Instance ZEquality: @Equality Z:= (@eq Z).*)
+
 (** Two generic morphisms from Z to (abrbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
- Variable R : Type.
- Variable Rr: Ring R.
-Existing Instance Rr.
- 
- Ltac rrefl := gen_reflexivity Rr.
+Context {R:Type}`{Ring R}.
 
-(*
-Print HintDb typeclass_instances.
-Print Scopes.
-*)
+ Ltac rrefl := reflexivity.
 
  Fixpoint gen_phiPOS1 (p:positive) : R :=
   match p with
@@ -86,15 +89,15 @@ Print Scopes.
   | _ => None
   end.
 
-   Ltac norm := gen_ring_rewrite.
+   Ltac norm := gen_rewrite.
    Ltac add_push :=  gen_add_push.
-Ltac rsimpl := simpl;  set_ring_notations.
+Ltac rsimpl := simpl.
 
  Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
  Proof.
   induction x;rsimpl.
-  ring_rewrite IHx. destruct x;simpl;norm.
-  ring_rewrite IHx;destruct x;simpl;norm.
+  rewrite IHx. destruct x;simpl;norm.
+  rewrite IHx;destruct x;simpl;norm.
   gen_reflexivity.
  Qed.
 
@@ -102,7 +105,7 @@ Ltac rsimpl := simpl;  set_ring_notations.
    gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
  Proof.
   induction x;rsimpl;norm.
-  ring_rewrite IHx ;norm.
+  rewrite IHx ;norm.
   add_push 1;gen_reflexivity.
  Qed.
 
@@ -110,39 +113,39 @@ Ltac rsimpl := simpl;  set_ring_notations.
    gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
  Proof.
   induction x;destruct y;simpl;norm.
-  ring_rewrite Pplus_carry_spec.
-  ring_rewrite ARgen_phiPOS_Psucc.
-  ring_rewrite IHx;norm.
+  rewrite Pplus_carry_spec.
+  rewrite ARgen_phiPOS_Psucc.
+  rewrite IHx;norm.
   add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity.
-  ring_rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity.
-  ring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
-  ring_rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity.
-  ring_rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity.
+  rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity.
+  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+  rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity.
+  rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity.
   add_push 1;gen_reflexivity.
-  ring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
  Qed.
 
  Lemma ARgen_phiPOS_mult :
    forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
  Proof.
   induction x;intros;simpl;norm.
-  ring_rewrite ARgen_phiPOS_add;simpl;ring_rewrite IHx;norm.
-  ring_rewrite IHx;gen_reflexivity.
+  rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
+  rewrite IHx;gen_reflexivity.
  Qed.
 
 
 (*morphisms are extensionaly equal*)
  Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
  Proof.
-  destruct x;rsimpl; try ring_rewrite same_gen; gen_reflexivity.
+  destruct x;rsimpl; try rewrite same_gen; gen_reflexivity.
  Qed.
 
  Lemma gen_Zeqb_ok : forall x y,
    Zeq_bool x y = true -> [x] == [y].
  Proof.
-  intros x y H.
-  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
-  ring_rewrite H1;gen_reflexivity.
+  intros x y H7.
+  assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10.
+  rewrite H10;gen_reflexivity.
  Qed.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
@@ -151,21 +154,52 @@ Ltac rsimpl := simpl;  set_ring_notations.
  Proof.
   intros x y.
   rewrite Z.pos_sub_spec.
-  assert (H0 := Pminus_mask_Gt x y). unfold Pos.gt in H0.
-  assert (H1 := Pminus_mask_Gt y x). unfold Pos.gt in H1.
-  rewrite Pos.compare_antisym in H1.
-  destruct (Pos.compare_spec x y) as [H|H|H].
-  subst. ring_rewrite ring_opp_def;gen_reflexivity.
-  destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; ring_rewrite Heq1;rewrite <- Heq2.
-  ring_rewrite ARgen_phiPOS_add;simpl;norm.
-  ring_rewrite ring_opp_def;norm.
-  destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
-  ring_rewrite ARgen_phiPOS_add;simpl;norm.
-  set_ring_notations. add_push (gen_phiPOS1 h). ring_rewrite ring_opp_def ; norm.
+  assert (HH0 := Pminus_mask_Gt x y). unfold Pos.gt in HH0.
+  assert (HH1 := Pminus_mask_Gt y x). unfold Pos.gt in HH1.
+  rewrite Pos.compare_antisym in HH1.
+  destruct (Pos.compare_spec x y) as [HH|HH|HH].
+  subst. rewrite ring_opp_def;gen_reflexivity.
+  destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial.
+  unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
+  rewrite ARgen_phiPOS_add;simpl;norm.
+  rewrite ring_opp_def;norm.
+  destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial.
+  unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
+  rewrite ARgen_phiPOS_add;simpl;norm.
+  add_push (gen_phiPOS1 h). rewrite ring_opp_def ; norm.
  Qed.
-
+(*
+Lemma gen_phiZ1_add_pos_neg : forall x y,
+ gen_phiZ1
+    match Pos.compare_cont x y Eq with
+    | Eq => Z0
+    | Lt => Zneg (y - x)
+    | Gt => Zpos (x - y)
+    end
+ == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Proof.
+  intros x y.
+  assert (HH:= (Pcompare_Eq_eq x y)); assert (HH0 := Pminus_mask_Gt x y).
+  generalize (Pminus_mask_Gt y x).
+  replace Eq with (CompOpp Eq);[intro HH1;simpl|trivial].
+  assert (Pos.compare_cont x y Eq = Gt -> (x > y)%positive).
+  auto with *.
+  assert (CompOpp(Pos.compare_cont x y Eq) = Gt -> (y > x)%positive).
+  rewrite Pcompare_antisym . simpl.
+  auto with *.
+  destruct (Pos.compare_cont x y Eq).
+  rewrite HH;trivial. rewrite ring_opp_def. rrefl.
+  destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial. simpl in H8. auto.
+  
+  unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
+  rewrite ARgen_phiPOS_add;simpl;norm.
+  rewrite ring_opp_def;norm.
+  destruct HH0 as [h [HHeq1 [HHeq2 HHor]]];trivial. auto.
+  unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
+  rewrite ARgen_phiPOS_add;simpl;norm.
+  add_push (gen_phiPOS1 h);rewrite ring_opp_def; norm.
+ Qed.
+*)
  Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
   match CompOpp x with Eq => be | Lt => bl | Gt => bg end
   = match x with Eq => be | Lt => bg | Gt => bl end.
@@ -173,45 +207,47 @@ Ltac rsimpl := simpl;  set_ring_notations.
 
  Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
  Proof.
-  intros x y; repeat ring_rewrite same_genZ; generalize x y;clear x y.
+  intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
-  apply gen_phiZ1_add_pos_neg.
-  rewrite gen_phiZ1_add_pos_neg.
-  ring_rewrite ring_add_comm. norm.
-  ring_rewrite ARgen_phiPOS_add; norm.
- Qed.
+  apply gen_phiZ1_add_pos_neg. 
+   rewrite gen_phiZ1_add_pos_neg. rewrite ring_add_comm.
+reflexivity.
+ rewrite ARgen_phiPOS_add. rewrite ring_opp_add. reflexivity.
+Qed.
 
 Lemma gen_phiZ_opp : forall x, [- x] == - [x].
  Proof.
-  intros x. repeat ring_rewrite same_genZ. generalize x ;clear x.
+  intros x. repeat rewrite same_genZ. generalize x ;clear x.
   induction x;simpl;norm.
-  ring_rewrite ring_opp_opp.  gen_reflexivity.
+  rewrite ring_opp_opp.  gen_reflexivity.
  Qed.
 
  Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
  Proof.
-  intros x y;repeat ring_rewrite same_genZ.
+  intros x y;repeat rewrite same_genZ.
   destruct x;destruct y;simpl;norm;
-  ring_rewrite  ARgen_phiPOS_mult;try (norm;fail).
-  ring_rewrite ring_opp_opp ;gen_reflexivity.
+  rewrite  ARgen_phiPOS_mult;try (norm;fail).
+  rewrite ring_opp_opp ;gen_reflexivity.
  Qed.
 
  Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
  Proof. intros;subst;gen_reflexivity. Qed.
 
 (*proof that [.] satisfies morphism specifications*)
- Lemma gen_phiZ_morph : @Ring_morphism Z R Zr Rr.
- apply (Build_Ring_morphism Zr Rr gen_phiZ);simpl;try gen_reflexivity.
-   apply gen_phiZ_add. intros. ring_rewrite ring_sub_def. 
-replace (x-y)%Z with (x + (-y))%Z. ring_rewrite gen_phiZ_add. 
-ring_rewrite gen_phiZ_opp. gen_reflexivity.
+Global Instance gen_phiZ_morph :
+(@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
+ apply Build_Ring_morphism; simpl;try gen_reflexivity.
+   apply gen_phiZ_add. intros. rewrite ring_sub_def. 
+replace (Zminus x y) with (x + (-y))%Z. rewrite gen_phiZ_add. 
+rewrite gen_phiZ_opp.  rewrite ring_sub_def. gen_reflexivity.
 reflexivity.
  apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. 
  Defined.
 
 End ZMORPHISM.
 
-
+Instance multiplication_phi_ring{R:Type}`{Ring R} : Multiplication  :=
+  {multiplication x y := (gen_phiZ x) * y}.
 
 
diff --git a/plugins/setoid_ring/Ring2_polynom.v b/plugins/setoid_ring/Ring2_polynom.v
index fdf5ca545..969220e89 100644
--- a/plugins/setoid_ring/Ring2_polynom.v
+++ b/plugins/setoid_ring/Ring2_polynom.v
@@ -14,29 +14,16 @@ Require Import BinList.
 Require Import BinPos.
 Require Import BinNat.
 Require Import BinInt.
+Require Export Ring_polynom. (* n'utilise que PExpr *)
 Require Export Ring2.
 
 Section MakeRingPol.
 
-Variable C:Type.
-Variable Cr:Ring C.
-Variable R:Type.
-Variable Rr:Ring R.
-
-Variable phi:@Ring_morphism C R Cr Rr.
-
-Existing Instance Rr.
-Existing Instance Cr.
-Existing Instance phi.
-(* marche pas avec x * [c] == [c] * x
-ou avec 
-Variable c:C.
-Variable x:C.
-Check [c]*x.
- *)
- Variable phiCR_comm: forall (c:C)(x:R), x * [c] == ring_mult [c] x.
+Context (C R:Type) `{Rh:Ring_morphism C R}.
+
+Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.
 
- Ltac rsimpl := repeat (gen_ring_rewrite || ring_rewrite phiCR_comm).
+ Ltac rsimpl := repeat (gen_rewrite || phiCR_comm).
  Ltac add_push := gen_add_push .
 
 (* Definition of non commutative multivariable polynomials 
@@ -47,11 +34,11 @@ Check [c]*x.
   | Pc : C -> Pol
   | PX : Pol -> positive -> positive -> Pol -> Pol. 
     (* PX P i n Q represents P * X_i^n + Q *)
-Definition cO := @ring0 _ Cr.
-Definition cI := @ring1 _ Cr.
+Definition cO:C . exact ring0. Defined.
+Definition cI:C . exact ring1. Defined.
 
- Definition P0 := Pc cO.
- Definition P1 := Pc cI.
+ Definition P0 := Pc 0.
+ Definition P1 := Pc 1.
 
 Variable Ceqb:C->C->bool.
 Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
@@ -65,7 +52,7 @@ Instance equalityb_coef : Equalityb C :=
   match P, P' with
   | Pc c, Pc c' => c =? c'
   | PX P i n Q, PX P' i' n' Q' =>
-    match Pos.compare i i', Pos.compare n n' with
+    match Pcompare i i' Eq, Pcompare n n' Eq with
     | Eq, Eq => if Peq P P' then Peq Q Q' else false
     | _,_ => false
     end
@@ -78,9 +65,9 @@ Instance equalityb_pol : Equalityb Pol :=
 (* Q a ses variables de queue < i *)
  Definition mkPX P i n Q :=
   match P with
-  | Pc c => if c =? cO then Q else PX P i n Q 
+  | Pc c => if c =? 0 then Q else PX P i n Q 
   | PX P' i' n' Q' => 
-       match Pos.compare i i' with
+       match Pcompare i i' Eq with
         | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q
         | _ => PX P i n Q
        end
@@ -116,13 +103,13 @@ Variable P:Pol.
 
 (* Xi^n * P + Q
 les variables de tete de Q ne sont pas forcement < i 
-mais Q est normalisé : variables de tete decroissantes *)
+mais Q est normalisé : variables de tete decroissantes *)
 
 Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
   match Q with
   | Pc c => mkPX P i n Q
   | PX P' i' n' Q' => 
-      match Pos.compare i i' with
+      match Pcompare i i' Eq with
       | (* i > i' *)
         Gt => mkPX P i n Q
       | (* i < i' *)
@@ -163,8 +150,8 @@ Definition Psub(P P':Pol):= P ++ (--P').
   end.
 
  Definition PmulC P c :=
-  if c =? cO then P0 else
-  if c =? cI then P else PmulC_aux P c.
+  if c =? 0 then P0 else
+  if c =? 1 then P else PmulC_aux P c.
 
  Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol :=
    match P2 with
@@ -185,7 +172,7 @@ Definition Psub(P P':Pol):= P ++ (--P').
   | Pc c => [c]
   | PX P i n Q =>
      let x := nth 0 i l in
-     let xn := pow_pos Rr x n in
+     let xn := pow_pos x n in
    (Pphi l P) * xn + (Pphi l Q)
   end.
 
@@ -201,16 +188,22 @@ Definition Psub(P P':Pol):= P ++ (--P').
  Proof.
   induction x;destruct y.
   replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
-  replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial.
+  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;
+rewrite Hh;trivial.
+  replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));
+trivial.
+  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;
+rewrite Hh;trivial.
   apply Pplus_xI_double_minus_one.
   simpl;trivial.
-  replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial.
+  replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));
+trivial.
+  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;
+rewrite Hh;trivial.
   apply Pplus_xI_double_minus_one.
   replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
-  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
+  assert (Hh := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite Hh;
+trivial.
   replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
   rewrite <- Pplus_one_succ_l.
   rewrite Psucc_o_double_minus_one_eq_xO;trivial.
@@ -224,47 +217,51 @@ Definition Psub(P P':Pol):= P ++ (--P').
  Lemma Peq_ok : forall P P',
     (P =? P') = true -> forall l, P@l == P'@ l.
  Proof.
-  induction P;destruct P';simpl;intros;try discriminate;trivial. apply ring_morphism_eq.
-  apply Ceqb_eq ;trivial.
-  destruct (Pos.compare_spec p p1); try discriminate H.
-  destruct (Pos.compare_spec p0 p2); try discriminate H.
-  assert (H1' := IHP1 P'1);assert (H2' := IHP2 P'2).
-  simpl in H1'. destruct (Peq P2 P'1); try discriminate H.
-  simpl in H2'. destruct (Peq P3 P'2); try discriminate H.
-  ring_rewrite (H1');trivial . ring_rewrite (H2');trivial.
-  subst. rrefl.
+  induction P;destruct P';simpl;intros;try discriminate;trivial.
+ apply ring_morphism_eq.
+ apply Ceqb_eq ;trivial.
+  assert (H1h := IHP1 P'1);assert (H2h := IHP2 P'2).
+   simpl in H1h. destruct (Peq P2 P'1). simpl in H2h; 
+destruct (Peq P3 P'2).
+  rewrite (H1h);trivial . rewrite (H2h);trivial. 
+assert (H3h := Pcompare_Eq_eq p p1);
+ destruct (Pos.compare_cont p p1 Eq);
+assert (H4h := Pcompare_Eq_eq p0 p2);
+destruct (Pos.compare_cont p0 p2 Eq); try (discriminate H).
+ rewrite H3h;trivial. rewrite H4h;trivial. reflexivity.
+ destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq);
+ try (discriminate H).
+ destruct (Pos.compare_cont p p1 Eq); destruct (Pos.compare_cont p0 p2 Eq);
+ try (discriminate H). 
  Qed.
 
  Lemma Pphi0 : forall l, P0@l == 0.
  Proof.
-  intros;simpl. unfold cO. ring_rewrite ring_morphism0. rrefl.
+  intros;simpl. 
+ rewrite ring_morphism0. reflexivity.
  Qed.
 
  Lemma Pphi1 : forall l,  P1@l == 1.
  Proof.
-  intros;simpl; unfold cI; ring_rewrite ring_morphism1. rrefl.
+  intros;simpl; rewrite ring_morphism1. reflexivity.
  Qed.
 
- Let pow_pos_Pplus :=
-    pow_pos_Pplus Rr.
-
  Lemma mkPX_ok : forall l P i n Q,
-  (mkPX P i n Q)@l == P@l * (pow_pos Rr (nth 0 i l) n) + Q@l.
+  (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l.
  Proof.
   intros l P i n Q;unfold mkPX.
-  destruct P;try (simpl;rrefl).
-  assert (H := ring_morphism_eq  c cO). simpl; case_eq (Ceqb c cO);simpl;try rrefl.
+  destruct P;try (simpl;reflexivity).
+  assert (Hh := ring_morphism_eq  c 0). 
+simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
 intros.
-  ring_rewrite H. ring_rewrite ring_morphism0.
-  rsimpl. apply Ceqb_eq. trivial.
-  case Pos.compare_spec; intros; subst.
-  assert (H := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl.
-  ring_rewrite H; trivial.
-  ring_rewrite Pphi0. rsimpl. ring_rewrite Pplus_comm.
-  ring_rewrite pow_pos_Pplus;rsimpl; trivial.
-  rrefl.
-  rrefl.
-  rrefl.
+  rewrite Hh. rewrite ring_morphism0.
+  rsimpl. apply Ceqb_eq. trivial. assert (Hh1 := Pcompare_Eq_eq i p);
+destruct (Pos.compare_cont i p Eq).
+  assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. 
+  rewrite Hh. 
+  rewrite Pphi0. rsimpl. rewrite Pplus_comm. rewrite pow_pos_Pplus;rsimpl.
+rewrite Hh1;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity.
+ simpl. reflexivity.
  Qed.
 
 Ltac Esimpl :=
@@ -272,60 +269,61 @@ Ltac Esimpl :=
    match goal with
    | |- context [?P@?l] =>
        match P with
-       | P0 => ring_rewrite (Pphi0 l)
-       | P1 => ring_rewrite (Pphi1 l)
-       | (mkPX ?P ?i ?n ?Q) => ring_rewrite (mkPX_ok l P i n Q)
+       | P0 => rewrite (Pphi0 l)
+       | P1 => rewrite (Pphi1 l)
+       | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q)
        end
    | |- context [[?c]] =>
        match c with
-       | cO => ring_rewrite ring_morphism0
-       | cI => ring_rewrite ring_morphism1
-       | ?x + ?y => ring_rewrite ring_morphism_add
-       | ?x * ?y => ring_rewrite ring_morphism_mul
-       | ?x - ?y => ring_rewrite ring_morphism_sub
-       | - ?x => ring_rewrite ring_morphism_opp
+       | 0 => rewrite ring_morphism0
+       | 1 => rewrite ring_morphism1
+       | ?x + ?y => rewrite ring_morphism_add
+       | ?x * ?y => rewrite ring_morphism_mul
+       | ?x - ?y => rewrite ring_morphism_sub
+       | - ?x => rewrite ring_morphism_opp
        end
    end));
-  ring_simpl; rsimpl.
+  simpl; rsimpl.
 
  Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
  Proof.
-  induction P; ring_simpl; intros; Esimpl; try rrefl. 
-  ring_rewrite IHP2. rsimpl. 
-ring_rewrite (ring_add_comm  (P2 @ l * pow_pos Rr (nth 0 p l) p0) [c]).
-rrefl.
+  induction P; simpl; intros; Esimpl; try reflexivity.
+ rewrite IHP2. rsimpl. 
+rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) [c]).
+reflexivity.
  Qed.
 
  Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l ==  P@l * [c].
  Proof.
-  induction P;ring_simpl;intros;Esimpl;try rrefl.
-  ring_rewrite IHP1;ring_rewrite IHP2;rsimpl. 
- Qed.
+  induction P;simpl;intros.  rewrite ring_morphism_mul.
+try reflexivity.
+  simpl. Esimpl.  rewrite IHP1;rewrite IHP2;rsimpl. 
+  repeat rewrite  phiCR_comm. Esimpl.  Qed.
 
  Lemma PmulC_ok : forall c P l, (PmulC P c)@l ==  P@l * [c].
  Proof.
   intros c P l; unfold PmulC.
-  assert (H:= ring_morphism_eq c cO);case_eq (c =? cO). intros.
-  ring_rewrite H;Esimpl. apply Ceqb_eq;trivial. 
-  assert (H1:= ring_morphism_eq c cI);case_eq (c =? cI);intros.
-  ring_rewrite H1;Esimpl. apply Ceqb_eq;trivial.
+  assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). intros.
+  rewrite Hh;Esimpl. apply Ceqb_eq;trivial. 
+  assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros.
+  rewrite H1h;Esimpl. apply Ceqb_eq;trivial.
   apply PmulC_aux_ok.
  Qed.
 
  Lemma Popp_ok : forall P l, (--P)@l == - P@l.
  Proof.
-  induction P;ring_simpl;intros.
+  induction P;simpl;intros.
   Esimpl.
-  ring_rewrite IHP1;ring_rewrite IHP2;rsimpl.
+  rewrite IHP1;rewrite IHP2;rsimpl.
  Qed.
 
  Ltac Esimpl2 :=
   Esimpl;
   repeat (progress (
    match goal with
-   | |- context [(PaddCl ?c ?P)@?l] => ring_rewrite (PaddCl_ok c P l)
-   | |- context [(PmulC ?P ?c)@?l] => ring_rewrite (PmulC_ok c P l)
-   | |- context [(--?P)@?l] => ring_rewrite (Popp_ok P l)
+   | |- context [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_ok c P l)
+   | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l)
+   | |- context [(--?P)@?l] => rewrite (Popp_ok P l)
    end)); Esimpl.
 
 Lemma PaddXPX: forall P i n Q,
@@ -333,7 +331,7 @@ Lemma PaddXPX: forall P i n Q,
   match Q with
   | Pc c => mkPX P i n Q
   | PX P' i' n' Q' => 
-      match Pos.compare i i' with
+      match Pcompare i i' Eq with
       | (* i > i' *)
         Gt => mkPX P i n Q
       | (* i < i' *)
@@ -357,46 +355,49 @@ Lemma PaddX_ok2 : forall P2,
    /\
    (forall P k n l,
            (PaddX Padd P2 k n P) @ l == 
-             P2 @ l * pow_pos Rr (nth 0 k l) n  + P @ l).
-induction P2;ring_simpl;intros. split. intros. apply PaddCl_ok.
- induction P.  unfold PaddX. intros. ring_rewrite mkPX_ok.
- ring_simpl. rsimpl.
-intros. ring_simpl.
- case Pos.compare_spec; intros; subst.
- assert (H1 := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2.
- rewrite H1. rrefl.
-ring_simpl. ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2.
- rewrite Pplus_comm in H1.
-rewrite H1. 
-ring_rewrite pow_pos_Pplus.  Esimpl2.
-ring_rewrite mkPX_ok. ring_rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1.
-rewrite H1.  Esimpl2. ring_rewrite pow_pos_Pplus. Esimpl2.
-ring_rewrite mkPX_ok. ring_rewrite IHP2. Esimpl2.
-ring_rewrite (ring_add_comm  (P2 @ l * pow_pos Rr (nth 0 p l) p0) 
-                             ([c] * pow_pos Rr (nth 0 k l) n)).
-rrefl.  assert (H1 := ring_morphism_eq c cO);case_eq (Ceqb c  cO); 
- intros; ring_simpl.
-ring_rewrite H1;trivial. Esimpl2. apply Ceqb_eq; trivial. rrefl.
+             P2 @ l * pow_pos (nth 0 k l) n  + P @ l).
+induction P2;simpl;intros. split. intros. apply PaddCl_ok.
+ induction P.  unfold PaddX. intros. rewrite mkPX_ok.
+ simpl. rsimpl.
+intros. simpl. assert (Hh := Pcompare_Eq_eq k p);
+ destruct (Pos.compare_cont k p Eq).
+ assert (H1h := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2.
+rewrite Hh; trivial. rewrite H1h. reflexivity.
+simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2.
+ rewrite Pplus_comm in H1h.
+rewrite H1h. 
+rewrite pow_pos_Pplus.  Esimpl2.
+rewrite Hh; trivial. reflexivity.
+rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1h.
+rewrite H1h.  Esimpl2. rewrite pow_pos_Pplus. Esimpl2.
+rewrite Hh; trivial. reflexivity.
+rewrite mkPX_ok. rewrite IHP2. Esimpl2.
+rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) 
+                             ([c] * pow_pos (nth 0 k l) n)).
+reflexivity.  assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c  0); 
+ intros; simpl.
+rewrite H1h;trivial. Esimpl2. apply Ceqb_eq; trivial. reflexivity.
 decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2.
-split. intros. ring_rewrite H0. ring_rewrite H1.
+split. intros. rewrite H0. rewrite H1.
 Esimpl2.
-induction P. unfold PaddX. intros. ring_rewrite mkPX_ok. ring_simpl. rrefl.
-intros. ring_rewrite PaddXPX. 
-case Pos.compare_spec; intros; subst.
-assert (H4 := ZPminus_spec n p2);destruct (ZPminus n p2). 
-ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. Esimpl2.
-rewrite H4. rrefl.
-ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2.
-rewrite Pplus_comm in H4.
-rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2.
-ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. 
-ring_rewrite mkPX_ok.
- Esimpl2.
- rewrite Pplus_comm in H4.
-rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2.
-ring_rewrite mkPX_ok. ring_simpl. ring_rewrite IHP2. Esimpl2.
-gen_add_push (P2 @ l * pow_pos Rr (nth 0 p1 l) p2). try rrefl.
-ring_rewrite mkPX_ok. ring_simpl. rrefl.
+induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity.
+intros. rewrite PaddXPX. 
+assert (H3h := Pcompare_Eq_eq k p1);
+ destruct (Pos.compare_cont k p1 Eq).
+assert (H4h := ZPminus_spec n p2);destruct (ZPminus n p2). 
+rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2.
+rewrite H4h. rewrite H3h;trivial. reflexivity.
+rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial.
+rewrite Pplus_comm in H4h.
+rewrite H4h. rewrite pow_pos_Pplus. Esimpl2.
+rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. 
+rewrite mkPX_ok.
+ Esimpl2. rewrite H3h;trivial.
+ rewrite Pplus_comm in H4h.
+rewrite H4h. rewrite pow_pos_Pplus. Esimpl2.
+rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2.
+gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity.
+rewrite mkPX_ok. simpl. reflexivity.
 Qed.
 
 Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l.
@@ -404,17 +405,17 @@ intro P. elim (PaddX_ok2 P); auto.
 Qed.
 
 Lemma PaddX_ok : forall P2 P k n l,
-   (PaddX Padd P2 k n P) @ l ==  P2 @ l * pow_pos Rr (nth 0 k l) n  + P @ l.
+   (PaddX Padd P2 k n P) @ l ==  P2 @ l * pow_pos (nth 0 k l) n  + P @ l.
 intro P2. elim (PaddX_ok2 P2); auto.
 Qed.
 
  Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
-unfold Psub. intros. ring_rewrite Padd_ok. ring_rewrite Popp_ok. rsimpl.
+unfold Psub. intros. rewrite Padd_ok. rewrite Popp_ok. rsimpl.
  Qed.
 
  Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
-induction P'; ring_simpl; intros. ring_rewrite PmulC_ok. rrefl.
-ring_rewrite PaddX_ok. ring_rewrite IHP'1. ring_rewrite IHP'2. Esimpl2.
+induction P'; simpl; intros. rewrite PmulC_ok. reflexivity.
+rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. Esimpl2.
 Qed.
 
  Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
@@ -424,6 +425,7 @@ Qed.
 
  (** Definition of polynomial expressions *)
 
+(*
  Inductive PExpr : Type :=
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
@@ -432,6 +434,7 @@ Qed.
   | PEmul : PExpr -> PExpr -> PExpr
   | PEopp : PExpr -> PExpr
   | PEpow : PExpr -> N -> PExpr.
+*)
 
  (** Specification of the power function *)
  Section POWER.
@@ -440,7 +443,7 @@ Qed.
   Variable rpow : R -> Cpow -> R.
 
   Record power_theory : Prop := mkpow_th {
-    rpow_pow_N : forall r n,  (rpow r (Cp_phi n))== (pow_N Rr r n)
+    rpow_pow_N : forall r n,  (rpow r (Cp_phi n))== (pow_N r n)
   }.
 
  End POWER.
@@ -450,7 +453,7 @@ Qed.
  Variable pow_th : power_theory Cp_phi rpow.
 
  (** evaluation of polynomial expressions towards R *)
- Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
+ Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
    match pe with
    | PEc c => [c]
    | PEX j => nth 0 j l
@@ -469,14 +472,14 @@ Strategy expand [PEeval].
 
  Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
  Proof.
-  destruct p;ring_simpl;intros;Esimpl;trivial.
+  destruct p;simpl;intros;Esimpl;trivial.
  Qed.
 
  Ltac Esimpl3 :=
   repeat match goal with
-  | |- context [(?P1 ++ ?P2)@?l] => ring_rewrite (Padd_ok P1 P2 l)
-  | |- context [(?P1 -- ?P2)@?l] => ring_rewrite (Psub_ok P1 P2 l)
-  end;try Esimpl2;try rrefl;try apply ring_add_comm.
+  | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P1 P2 l)
+  | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l)
+  end;try Esimpl2;try reflexivity;try apply ring_add_comm.
 
 (* Power using the chinise algorithm *)
 
@@ -506,11 +509,11 @@ Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
          forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l.
   Proof.
    intros l subst_l_ok res P p. generalize res;clear res.
-   induction p;ring_simpl;intros. try ring_rewrite subst_l_ok.
- repeat ring_rewrite Pmul_ok. repeat ring_rewrite IHp.
-   rsimpl. repeat ring_rewrite Pmul_ok. repeat ring_rewrite IHp. rsimpl.
- try ring_rewrite subst_l_ok.
- repeat ring_rewrite Pmul_ok. rrefl.
+   induction p;simpl;intros. try rewrite subst_l_ok.
+ repeat rewrite Pmul_ok. repeat rewrite IHp.
+   rsimpl. repeat rewrite Pmul_ok. repeat rewrite IHp. rsimpl.
+ try rewrite subst_l_ok.
+ repeat rewrite Pmul_ok. reflexivity.
   Qed.
 
 Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
@@ -521,7 +524,7 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
 
   Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
          forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l.
-  Proof.  destruct n;ring_simpl. rrefl. ring_rewrite Ppow_pos_ok; trivial. Esimpl.  Qed.
+  Proof.  destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl.  Qed.
 
  End POWER2.
 
@@ -532,7 +535,7 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
   Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
   Let Ppow_subst := Ppow_N subst_l.
 
-  Fixpoint norm_aux (pe:PExpr) : Pol :=
+  Fixpoint norm_aux (pe:PExpr C) : Pol :=
    match pe with
    | PEc c => Pc c
    | PEX j => mk_X j
@@ -554,27 +557,27 @@ Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
   Proof.
    intros.
    induction pe.
-Esimpl3. Esimpl3. ring_simpl.
- ring_rewrite IHpe1;ring_rewrite IHpe2.
+Esimpl3. Esimpl3. simpl.
+ rewrite IHpe1;rewrite IHpe2.
  destruct pe2; Esimpl3. 
 unfold Psub.
-destruct pe1. destruct pe2. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
- Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
-ring_simpl. unfold Psub. ring_rewrite IHpe1;ring_rewrite IHpe2.
-destruct pe1. destruct pe2. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+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.
-ring_simpl. ring_rewrite IHpe1;ring_rewrite IHpe2. ring_rewrite Pmul_ok. rrefl.
-ring_simpl. ring_rewrite IHpe; Esimpl3. 
-ring_simpl.
-   ring_rewrite Ppow_N_ok; (intros;try rrefl). 
-   ring_rewrite rpow_pow_N.  Esimpl3.
-   induction n;ring_simpl. Esimpl3. induction p; ring_simpl.
-  try ring_rewrite IHp;try ring_rewrite IHpe;
- repeat ring_rewrite Pms_ok;
-      repeat ring_rewrite Pmul_ok;rrefl.
-ring_rewrite Pmul_ok. try ring_rewrite IHp;try ring_rewrite IHpe;
- repeat ring_rewrite Pms_ok;
-      repeat ring_rewrite Pmul_ok;rrefl. trivial.
+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.
   Qed.
 
@@ -588,7 +591,7 @@ exact pow_th.
 
  End NORM_SUBST_REC.
 
- Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop :=
+ Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop :=
    match lpe with
    | nil => True
    | (me,pe)::lpe =>
@@ -610,8 +613,8 @@ exact pow_th.
    (norm_subst pe1 =? norm_subst pe2) = true ->
    PEeval l pe1 == PEeval l pe2.
  Proof.
-  ring_simpl;intros.
-  do 2 (ring_rewrite (norm_subst_ok l);trivial).
+  simpl;intros.
+  do 2 (rewrite (norm_subst_ok l);trivial).
   apply Peq_ok;trivial.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ring2_tac.v
index c4dfe3169..fad36e571 100644
--- a/plugins/setoid_ring/Ring2_tac.v
+++ b/plugins/setoid_ring/Ring2_tac.v
@@ -13,7 +13,6 @@ Require Import BinList.
 Require Import Znumtheory.
 Require Export Morphisms Setoid Bool.
 Require Import ZArith.
-Open Scope Z_scope.
 Require Import Algebra_syntax.
 Require Export Ring2.
 Require Import Ring2_polynom.
@@ -22,176 +21,163 @@ Require Import Ring2_initial.
 
 Set Implicit Arguments.
 
-(* Reification with Type Classes, inspired from B.Grégoire and A.Spiewack *)
+Class nth (R:Type) (t:R) (l:list R) (i:nat).
 
-Class is_in_list_at (R:Type) (t:R) (l:list R) (i:nat) := {}.
 Instance  Ifind0 (R:Type) (t:R) l
- : is_in_list_at t (t::l) 0.
+ : nth t(t::l) 0.
+
 Instance  IfindS (R:Type) (t2 t1:R) l i 
- `{is_in_list_at R t1 l i} 
- : is_in_list_at t1 (t2::l) (S i) | 1.
-
-Class reifyPE (R:Type) (e:PExpr Z) (lvar:list R) (t:R) := {}.
-Instance  reify_zero (R:Type) (RR:Ring R) lvar 
- : reifyPE (PEc 0%Z) lvar ring0.
-Instance  reify_one (R:Type) (RR:Ring R) lvar 
- : reifyPE (PEc 1%Z) lvar ring1.
-Instance  reify_plus (R:Type)  (RR:Ring R)
-  e1 lvar t1 e2 t2 
- `{reifyPE R e1 lvar t1} 
- `{reifyPE R e2 lvar t2} 
- : reifyPE (PEadd e1 e2) lvar (ring_plus t1 t2).
-Instance  reify_mult (R:Type)  (RR:Ring R)
-  e1 lvar t1 e2 t2 
- `{reifyPE R e1 lvar t1} 
- `{reifyPE R e2 lvar t2}
- : reifyPE (PEmul e1 e2) lvar (ring_mult t1 t2).
-Instance  reify_sub (R:Type) (RR:Ring R) 
- e1 lvar t1 e2 t2 
- `{reifyPE R e1 lvar t1} 
- `{reifyPE R e2 lvar t2}
- : reifyPE (PEsub e1 e2) lvar (ring_sub t1 t2).
-Instance  reify_opp (R:Type) (RR:Ring R) 
- e1 lvar t1 
- `{reifyPE R e1 lvar t1}
- : reifyPE (PEopp e1) lvar (ring_opp t1).
+ {_:nth t1 l i} 
+ : nth t1 (t2::l) (S i) | 1.
+
+Class closed (T:Type) (l:list T).
+
+Instance Iclosed_nil T 
+ : closed (T:=T) nil.
+
+Instance Iclosed_cons T t (l:list T) 
+ {_:closed l} 
+ : closed (t::l).
+
+Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R).
+
+Instance  reify_zero (R:Type)  lvar op
+ `{Ring (T:=R)(ring0:=op)}
+ : reify (ring0:=op)(PEc 0%Z) lvar op.
+
+Instance  reify_one (R:Type)  lvar op
+ `{Ring (T:=R)(ring1:=op)}
+ : reify (ring1:=op) (PEc 1%Z) lvar op.
+
+Instance  reify_add (R:Type)
+  e1 lvar t1 e2 t2 op 
+ `{Ring (T:=R)(add:=op)}
+ {_:reify (add:=op) e1 lvar t1}
+ {_:reify (add:=op) e2 lvar t2}
+ : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2).
+
+Instance  reify_mul (R:Type) 
+  e1 lvar t1 e2 t2 op 
+ `{Ring (T:=R)(mul:=op)}
+ {_:reify (mul:=op) e1 lvar t1}
+ {_:reify (mul:=op) e2 lvar t2}
+ : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2).
+
+Instance  reify_mul_ext (R:Type) `{Ring R}
+  lvar z e2 t2 
+ `{Ring (T:=R)}
+ {_:reify e2 lvar t2}
+ : reify (PEmul (PEc z) e2) lvar
+      (@multiplication Z _ _  z t2)|9.
+
+Instance  reify_sub (R:Type)
+ e1 lvar t1 e2 t2 op
+ `{Ring (T:=R)(sub:=op)}
+ {_:reify (sub:=op) e1 lvar t1}
+ {_:reify (sub:=op) e2 lvar t2}
+ : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2).
+
+Instance  reify_opp (R:Type)
+ e1 lvar t1  op
+ `{Ring (T:=R)(opp:=op)}
+ {_:reify (opp:=op) e1 lvar t1}
+ : reify (opp:=op) (PEopp e1) lvar (op t1).
+
+Instance  reify_pow (R:Type) `{Ring R}
+ e1 lvar t1 n 
+ `{Ring (T:=R)}
+ {_:reify e1 lvar t1}
+ : reify (PEpow e1 n) lvar (pow_N t1 n)|1.
+
 Instance  reify_var (R:Type) t lvar i 
- `{is_in_list_at R t lvar i}
- : reifyPE (PEX Z (P_of_succ_nat i)) lvar t 
+ `{nth R t lvar i}
+ `{Rr: Ring (T:=R)}
+ : reify (Rr:= Rr) (PEX Z (P_of_succ_nat i))lvar t 
  | 100.
 
-Class reifyPElist (R:Type) (lexpr:list (PExpr Z)) (lvar:list R) 
-  (lterm:list R) := {}.
-Instance reifyPE_nil (R:Type) lvar 
- : @reifyPElist R nil lvar (@nil R).
-Instance reifyPE_cons (R:Type) e1 lvar t1 lexpr2 lterm2
- `{reifyPE R e1 lvar t1} `{reifyPElist R lexpr2 lvar lterm2} 
- : reifyPElist (e1::lexpr2) lvar (t1::lterm2).
+Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) 
+  (lterm:list R).
 
-Class is_closed_list T (l:list T) := {}.
-Instance Iclosed_nil T 
- : is_closed_list (T:=T) nil.
-Instance Iclosed_cons T t l 
- `{is_closed_list (T:=T) l} 
- : is_closed_list (T:=T) (t::l).
+Instance reify_nil (R:Type) lvar 
+ `{Rr: Ring (T:=R)}
+ : reifylist (Rr:= Rr) nil lvar (@nil R).
+
+Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2
+ `{Rr: Ring (T:=R)}
+ {_:reify (Rr:= Rr) e1 lvar t1}
+ {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} 
+ : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2).
 
 Definition list_reifyl (R:Type) lexpr lvar lterm 
- `{reifyPElist R lexpr lvar lterm}
- `{is_closed_list (T:=R) lvar} := (lvar,lexpr).
+ `{Rr: Ring (T:=R)}
+ {_:reifylist (Rr:= Rr) lexpr lvar lterm}
+ `{closed (T:=R) lvar}  := (lvar,lexpr).
 
 Unset Implicit Arguments.
 
-Instance multiplication_phi_ring{R:Type}{Rr:Ring R} : Multiplication  :=
-  {multiplication x y := ring_mult (gen_phiZ Rr x) y}.
-
-(*
-Print HintDb typeclass_instances.
-*)
-(* Reification *)
 
 Ltac lterm_goal g :=
   match g with
-  ring_eq ?t1 ?t2 => constr:(t1::t2::nil)
-  | ring_eq ?t1 ?t2 -> ?g => let lvar :=
-    lterm_goal g in constr:(t1::t2::lvar)     
+  | ?t1 == ?t2 => constr:(t1::t2::nil)
+  | ?t1 = ?t2 => constr:(t1::t2::nil)
   end.
 
+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;*)
+  (*idtac lvar; idtac lexpr; idtac lterm;*)
   match lexpr with
      nil => idtac
-   | ?e::?lexpr1 =>  
-        match lterm with
-         ?t::?lterm1 => (* idtac "t="; idtac t;*)
-           let x := fresh "T" in
-           set (x:= t);
-           change x with 
-             (@PEeval Z Zr _ _ (@gen_phiZ_morph _ _) N
-                      (fun n:N => n) (@Ring_theory.pow_N _ ring1 ring_mult)
-                      lvar e); 
-           clear x;
-           reify_goal lvar lexpr1 lterm1
+   | ?e1::?e2::_ =>  
+        match goal with
+          |- (?op ?u1 ?u2) =>
+           change (op 
+             (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
+                      (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
+                      lvar e1)
+             (@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
+                      (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
+                      lvar e2))
         end
   end.
 
-Existing Instance gen_phiZ_morph.
-Existing Instance Zr.
-
-Lemma comm: forall (R:Type)(Rr:Ring R)(c : Z) (x : R),
-  x * [c] == [c] * x.
-induction c. intros. ring_simpl. gen_ring_rewrite. simpl. intros.
-ring_rewrite_rev same_gen.
-induction p. simpl.  gen_ring_rewrite. ring_rewrite IHp. rrefl.
-simpl.  gen_ring_rewrite. ring_rewrite IHp. rrefl.
-simpl.  gen_ring_rewrite. 
-simpl. intros. ring_rewrite_rev same_gen.
+Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R),
+  x * (gen_phiZ c) == (gen_phiZ c) * x.
+induction c. intros. simpl. gen_rewrite. simpl. intros.
+rewrite <- same_gen.
+induction p. simpl.  gen_rewrite. rewrite IHp. reflexivity.
+simpl.  gen_rewrite. rewrite IHp. reflexivity.
+simpl.  gen_rewrite. 
+simpl. intros. rewrite <- same_gen.
 induction p. simpl. generalize IHp. clear IHp.
-gen_ring_rewrite. intro IHp.  ring_rewrite IHp. rrefl.
+gen_rewrite. intro IHp.  rewrite IHp. reflexivity.
 simpl. generalize IHp. clear IHp.
-gen_ring_rewrite. intro IHp.  ring_rewrite IHp. rrefl.
-simpl.  gen_ring_rewrite. Qed.
+gen_rewrite. intro IHp.  rewrite IHp. reflexivity.
+simpl.  gen_rewrite. Qed.
 
-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). rrefl. Qed. 
-
-
- Ltac ring_gen :=
+Ltac ring_gen :=
    match goal with
-     |- ?g => let lterm := lterm_goal g in (* les variables *)
+     |- ?g => let lterm := lterm_goal g in 
        match eval red in (list_reifyl (lterm:=lterm)) with
          | (?fv, ?lexpr) => 
-(*         idtac "variables:";idtac fv;
+           (*idtac "variables:";idtac fv;
            idtac "terms:"; idtac lterm;
-           idtac "reifications:"; idtac lexpr; 
-*)
+           idtac "reifications:"; idtac lexpr; *)
            reify_goal fv lexpr lterm;
            match goal with 
              |- ?g => 
-               set_ring_notations;
-               apply (@ring_correct Z Zr _ _ (@gen_phiZ_morph _ _)
-                 (@comm _ _) Zeq_bool Zeqb_ok N (fun n:N => n)
-                 (@Ring_theory.pow_N _  1 multiplication));
-               [apply mkpow_th; rrefl
+               apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
+                       (@gen_phiZ _ _ _ _ _ _ _ _ _) _
+                 (@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n)
+                 (@pow_N _ _ _ _ _ _ _ _ _));
+               [apply mkpow_th; reflexivity
                  |vm_compute; reflexivity]
            end
        end
    end.
 
-(* Pierre L: these tests should be done in a section, otherwise
-   global axioms are generated. Ideally such tests should go in
-   the test-suite directory *)
-Section Tests.
- 
 Ltac ring2:= 
-  unset_ring_notations; intros;
-  match goal with
-    |- (@ring_eq ?r ?rd _ _ ) =>
-          simpl; ring_gen
-  end.
-Variable R: Type.
-Variable Rr: Ring R.
-Existing Instance Rr.
-
-Goal forall x y z:R, x  == x .
-ring2. 
-Qed.
-
-Goal forall x y z:R, x * y * z == x * (y * z).
-ring2.
-Qed.
-
-Goal forall x y z:R, [3]* x *([2]* y * z) == [6] * (x * y) * z.
-ring2.
-Qed.
-
-Goal forall x y z:R, 3 * x * (2 * y * z) == 6 * (x * y) * z.
-ring2.
-Qed.
-
-
-(* Fails with Multiplication: A -> B -> C.
-Goal forall x:R,    2%Z * (x * x) == 3%Z * x.
-Admitted.
-*)
+  intros;
+  ring_gen.
 
-End Tests.
\ No newline at end of file
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index cccd21855..2b08f9400 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -15,8 +15,6 @@ Ring.vo
 ZArithRing.vo
 Algebra_syntax.vo
 Cring.vo
-Cring_initial.vo
-Cring_tac.vo
 Ring2.vo
 Ring2_polynom.vo
 Ring2_initial.vo