Ring2 devient Ncring et la reification par les type classes est partagee

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

11 files changed, 388 insertions, 669 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 6d5ea258b..ef1701c9f 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -12,6 +12,8 @@
  
 Examples: see test-suite/success/Nsatz.v
 
+Reification is done using type classes, defined in Ncring_tac.v
+
 *)
 
 Require Import List.
@@ -21,30 +23,17 @@ Require Import BinList.
 Require Import Znumtheory.
 Require Export Morphisms Setoid Bool.
 Require Export Algebra_syntax.
-Require Export Ring2.
-Require Export Ring2_initial.
-Require Export Ring2_tac.
-Require Export Cring.
+Require Export Ncring.
+Require Export Ncring_initial.
+Require Export Ncring_tac.
+Require Export Integral_domain.
 
 Declare ML Module "nsatz_plugin".
 
-(* Definition of integral domains: commutative ring without zero divisor *)
-
-Class Integral_domain {R : Type}`{Rcr:Cring R} := {
- integral_domain_product:
-   forall x y, x * y == 0 -> x == 0 \/ y == 0;
- integral_domain_one_zero: not (1 == 0)}.
-
-Section integral_domain.
+Section nsatz1.
 
 Context {R:Type}`{Rid:Integral_domain R}.
 
-Lemma integral_domain_minus_one_zero: ~ - (1:R) == 0.
-red;intro. apply integral_domain_one_zero. 
-assert (0 == - (0:R)). cring.
-rewrite H0. rewrite <- H. cring.
-Qed.
-
 Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y.
 intros x y H; setoid_replace x with ((x - y) + y); simpl;
  [setoid_rewrite H | idtac]; simpl. cring. cring.
@@ -107,8 +96,6 @@ Definition PhiR : list R -> PolZ -> R :=
   (Pphi ring0 add mul 
     (InitialRing.gen_phiZ ring0 ring1 add mul opp)).
 
-Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n).
-
 Definition PEevalR : list R -> PEZ -> R :=
    PEeval ring0 add mul sub opp
     (gen_phiZ ring0 ring1 add mul opp)
@@ -222,25 +209,6 @@ Qed.
 
 (* fin *)
 
-Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0.
-induction n. unfold pow; simpl. intros. absurd (1 == 0). 
-simpl. apply integral_domain_one_zero.
- trivial. setoid_replace (pow p (S n)) with (p * (pow p n)).
-intros. 
-case (integral_domain_product p (pow p n) H). trivial. trivial. 
-unfold pow; simpl. 
-clear IHn. induction n; simpl; try cring. 
- rewrite Ring_theory.pow_pos_Psucc. cring. exact Rset.
-apply ring_mult_comp.
-apply cring_mul_comm.
-apply ring_mul_assoc.
-Qed.
-
-Lemma Rintegral_domain_pow:
-  forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0.
-intros. case (integral_domain_product c (pow p r) H0). intros; absurd (c == ring0); auto. 
-intros. apply pow_not_zero with r. trivial. Qed.   
-
 Definition R2:= 1 + 1.
 
 Fixpoint IPR p {struct p}: R :=
@@ -278,7 +246,7 @@ Fixpoint interpret3 t fv {struct t}: R :=
   end.
 
 
-End integral_domain.
+End nsatz1.
 
 Ltac equality_to_goal H x y:=
   let h := fresh "nH" in
@@ -458,38 +426,6 @@ Tactic Notation "nsatz" "with"
     nsatz_generic radicalmax info lparam lvar
   end.
 
-Section test.
-Context {R:Type}`{Rid:Integral_domain R}.
-
-Goal forall x y:R, x == x.
-nsatz with radicalmax := 6%N strategy := 1%Z parameters := (@nil R)
- variables := (@nil R).
-Qed.
-
-Goal forall x y:R, x == y -> y*y == x*x.
-nsatz.
-Qed.
-
-Lemma example3 : forall x y z:R,
-  x+y+z==0 ->
-  x*y+x*z+y*z==0->
-  x*y*z==0 -> x*x*x==0.
-Proof.
-nsatz.
-Qed.
-(*
-Lemma example5 : forall x y z u v:R,
-  x+y+z+u+v==0 ->
-  x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0->
-  x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0->
-  x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 ->
-  x*y*z*u*v==0 -> x*x*x*x*x ==0.
-Proof.
-nsatz.
-Qed.
-*)
-End test.
-
 (* Real numbers *)
 Require Import Reals.
 Require Import RealField.
@@ -522,10 +458,6 @@ Instance Rdi : (Integral_domain (Rcr:=Rcri)).
 constructor. 
 exact Rmult_integral. exact R_one_zero. Defined.
 
-Goal forall x y:R, x = y -> (x*x-x+1)%R = ((y*y-y)+1+0)%R.
-nsatz.
-Qed.
-
 (* Rational numbers *)
 Require Import QArith.
 
@@ -554,10 +486,6 @@ Instance Qdi : (Integral_domain (Rcr:=Qcri)).
 constructor. 
 exact Qmult_integral. exact Q_one_zero. Defined.
 
-Goal forall x y:Q, Qeq x y -> Qeq (x*x-x+1)%Q ((y*y-y)+1+0)%Q.
-nsatz.
-Qed.
-
 (* Integers *)
 Lemma Z_one_zero: 1%Z <> 0%Z.
 omega. 
@@ -570,10 +498,3 @@ Instance Zdi : (Integral_domain (Rcr:=Zcri)).
 constructor. 
 exact Zmult_integral. exact Z_one_zero. Defined.
 
-Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z.
-nsatz. 
-Qed.
-
-Goal forall x y:Z, x = y -> x = x -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z.
-nsatz. 
-Qed.
\ No newline at end of file
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 1f7915eeb..3d6e53fcd 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -6,17 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import List.
+Require Export List.
 Require Import Setoid.
 Require Import BinPos.
 Require Import BinList.
 Require Import Znumtheory.
 Require Export Morphisms Setoid Bool.
-Require Import ZArith.
+Require Import ZArith_base.
 Require Export Algebra_syntax.
-Require Export Ring2.
-Require Export Ring2_initial.
-Require Export Ring2_tac.
+Require Export Ncring.
+Require Export Ncring_initial.
+Require Export Ncring_tac.
 
 Class Cring {R:Type}`{Rr:Ring R} := 
  cring_mul_comm: forall x y:R, x * y == y * x.
@@ -30,10 +30,10 @@ Ltac reify_goal lvar lexpr lterm:=
           |- (?op ?u1 ?u2) =>
            change (op 
              (@Ring_polynom.PEeval
-               _ zero _+_ _*_ _-_ -_ Z gen_phiZ N (fun n:N => n)
+               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.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)
+               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
                (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
         end
   end.
@@ -65,13 +65,13 @@ 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.
+             Ncring_initial.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 Ncring_initial.gen_phiZ_add; reflexivity.
+rewrite ring_sub_def. unfold Zminus. rewrite Ncring_initial.gen_phiZ_add.
+rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
+rewrite Ncring_initial.gen_phiZ_mul; reflexivity.
+rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
 rewrite (Zeqb_ok x y H). reflexivity. Defined.
 
 Lemma cring_power_theory : 
@@ -80,14 +80,15 @@ Lemma cring_power_theory :
 intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
 
 Lemma cring_div_theory: 
-  div_theory _==_ Zplus Zmult gen_phiZ Z.quotrem.
+  div_theory _==_ Zplus Zmult Ncring_initial.gen_phiZ Z.quotrem.
 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 *)
+    |- ?g => let lterm := lterm_goal g in
         match eval red in (list_reifyl (lterm:=lterm)) with
           | (?fv, ?lexpr) => 
            (*idtac "variables:";idtac fv;
@@ -102,7 +103,7 @@ Ltac cring_gen :=
                         cring_eq_ext
                         cring_almost_ring_theory
                         Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
-                        gen_phiZ
+                        Ncring_initial.gen_phiZ
                         cring_morph
                         N
                         (fun n:N => n)
@@ -124,3 +125,148 @@ Ltac cring:=
   cring_gen;
   cring_compute.
 
+Instance Zcri: (Cring (Rr:=Zr)).
+red. exact Zmult_comm. Defined.
+
+(* Cring_simplify *)
+
+Ltac cring_simplify_aux lterm fv lexpr hyp :=
+    match lterm with
+      | ?t0::?lterm =>
+    match lexpr with
+      | ?e::?le =>
+        let t := constr:(@Ring_polynom.norm_subst
+          Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool Z.quotrem O nil e) in
+        let te := 
+          constr:(@Ring_polynom.Pphi_dev
+            _ 0 1 _+_ _*_ _-_ -_ 
+            
+            Z 0%Z 1%Z Zeq_bool
+            Ncring_initial.gen_phiZ
+            get_signZ fv t) in
+        let eq1 := fresh "ring" in
+        let nft := eval vm_compute in t in
+        let t':= fresh "t" in
+        pose (t' := nft);
+        assert (eq1 : t = t');
+        [vm_cast_no_check (refl_equal t')|
+        let eq2 := fresh "ring" in
+        assert (eq2:(@Ring_polynom.PEeval
+          _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+          (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
+        [let eq3 := fresh "ring" in
+          generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_
+            ring_setoid
+            cring_eq_ext
+            cring_almost_ring_theory
+            Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+            Ncring_initial.gen_phiZ
+            cring_morph
+            N
+            (fun n:N => n)
+            (@Ring_theory.pow_N _ 1 multiplication)
+            cring_power_theory
+            Z.quotrem
+            cring_div_theory
+            get_signZ get_signZ_th
+            O nil fv I nil (refl_equal nil) );
+          intro eq3; apply eq3; reflexivity|
+              match hyp with
+                | 1%nat => rewrite eq2
+                | ?H => try rewrite eq2 in H
+              end];
+        let P:= fresh "P" in
+        match hyp with
+          | 1%nat => 
+            rewrite eq1;
+            pattern (@Ring_polynom.Pphi_dev
+            _ 0 1 _+_ _*_ _-_ -_ 
+            
+            Z 0%Z 1%Z Zeq_bool
+            Ncring_initial.gen_phiZ
+            get_signZ fv t');
+            match goal with
+              |- (?p ?t) => set (P:=p)
+            end;
+              unfold t' in *; clear t' eq1 eq2;
+              unfold Pphi_dev, Pphi_avoid; simpl;
+                repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
+                  mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
+                  mkpow;simpl)
+          | ?H =>
+               rewrite eq1 in H;
+               pattern (@Ring_polynom.Pphi_dev
+            _ 0 1 _+_ _*_ _-_ -_ 
+            
+            Z 0%Z 1%Z Zeq_bool
+            Ncring_initial.gen_phiZ
+            get_signZ fv t') in H; 
+               match type of H with
+                  | (?p ?t)  => set (P:=p) in H
+               end;
+               unfold t' in *; clear t' eq1 eq2;
+               unfold Pphi_dev, Pphi_avoid in H; simpl in H;
+                repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
+                  mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
+                  mkpow in H;simpl in H)
+        end; unfold P in *; clear P
+        ]; cring_simplify_aux lterm fv le hyp
+      | nil => idtac
+    end
+    | nil => idtac
+    end.
+
+Ltac set_variables fv :=
+  match fv with
+    | nil => idtac
+    | ?t::?fv =>
+        let v := fresh "X" in
+        set (v:=t) in *; set_variables fv
+  end.
+
+Ltac deset n:=
+   match n with
+    | 0%nat => idtac
+    | S ?n1 =>
+      match goal with
+        | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
+      end
+   end.
+
+(* a est soit un terme de l'anneau, soit une liste de termes.
+J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list
+ dans Tactic Notation *)
+
+Ltac cring_simplify_gen a hyp :=
+  let lterm :=
+    match a with
+      | _::_ => a
+      | _ => constr:(a::nil)
+    end in
+    match eval red in (list_reifyl (lterm:=lterm)) with
+      | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
+      let n := eval compute in (length fv) in
+      idtac n;
+      let lt:=fresh "lt" in
+      set (lt:= lterm);
+      let lv:=fresh "fv" in
+      set (lv:= fv);
+      (* les termes de fv sont remplacés par des variables 
+         pour pouvoir utiliser simpl ensuite sans risquer
+         des simplifications indésirables *)
+      set_variables fv;
+      let lterm1 := eval unfold lt in lt in
+      let lv1 := eval unfold lv in lv in
+        idtac lterm1; idtac lv1;
+      cring_simplify_aux lterm1 lv1 lexpr hyp;
+      clear lt lv;
+      (* on remet les termes de fv *)
+      deset n
+    end.
+
+Tactic Notation "cring_simplify" constr(lterm):=
+ cring_simplify_gen lterm 1%nat.
+
+Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):=
+ cring_simplify_gen lterm H.
+
diff --git a/plugins/setoid_ring/Cring_Q.v b/plugins/setoid_ring/Cring_Q.v
new file mode 100644
index 000000000..ca8439aa6
--- /dev/null
+++ b/plugins/setoid_ring/Cring_Q.v
@@ -0,0 +1,22 @@
+Require Export Cring.
+
+(* Rational numbers *)
+Require Import QArith.
+
+Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+
+Instance Qri : (Ring (Ro:=Qops)).
+constructor.
+try apply Q_Setoid. 
+apply Qplus_comp. 
+apply Qmult_comp. 
+apply Qminus_comp. 
+apply Qopp_comp.
+ exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc.
+ exact Qmult_1_l.  exact Qmult_1_r. apply Qmult_assoc.
+ apply Qmult_plus_distr_l.  intros. apply Qmult_plus_distr_r. 
+reflexivity. exact Qplus_opp_r.
+Defined.
+
+Instance Qcri: (Cring (Rr:=Qri)).
+red. exact Qmult_comm. Defined.
diff --git a/plugins/setoid_ring/Cring_R.v b/plugins/setoid_ring/Cring_R.v
new file mode 100644
index 000000000..b548aa7aa
--- /dev/null
+++ b/plugins/setoid_ring/Cring_R.v
@@ -0,0 +1,25 @@
+Require Export Cring.
+
+(* Real numbers *)
+Require Import Reals.
+Require Import RealField.
+
+Lemma Rsth : Setoid_Theory R (@eq R).
+constructor;red;intros;subst;trivial.
+Qed.
+
+Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+
+Instance Rri : (Ring (Ro:=Rops)).
+constructor;
+try (try apply Rsth;
+   try (unfold respectful, Proper; unfold equality; unfold eq_notation in *;
+  intros; try rewrite H; try rewrite H0; reflexivity)).
+ exact Rplus_0_l. exact Rplus_comm. symmetry. apply Rplus_assoc.
+ exact Rmult_1_l.  exact Rmult_1_r. symmetry. apply Rmult_assoc.
+ exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l. 
+exact Rplus_opp_r.
+Defined.
+
+Instance Rcri: (Cring (Rr:=Rri)).
+red. exact Rmult_comm. Defined.
diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v
deleted file mode 100644
index ca894027a..000000000
--- a/plugins/setoid_ring/Cring_initial.v
+++ /dev/null
@@ -1,217 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import ZArith_base.
-Require Import Zpow_def.
-Require Import BinInt.
-Require Import BinNat.
-Require Import Setoid.
-Require Import Algebra_syntax.
-Require Export Ring_polynom.
-Require Export Cring.
-Import List.
-
-Set Implicit Arguments.
-
-(* An object to return when an expression is not recognized as a constant *)
-Definition NotConstant := false.
-
-(** Z is a ring and a setoid*)
-
-Lemma Zsth : Setoid_Theory Z (@eq Z).
-constructor;red;intros;subst;trivial.
-Qed.
-
-Definition Zr : Cring Z.
-apply (@Build_Cring Z Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z)); 
-try apply Zsth; try (red; red; intros; rewrite H; reflexivity). 
- exact Zplus_comm. exact Zplus_assoc.
- exact Zmult_1_l.  exact Zmult_assoc. exact Zmult_comm.
- exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
-Defined.
-
-(** 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: Cring R.
-Existing Instance Rr.
- 
- Ltac rrefl := gen_reflexivity Rr.
-
-(*
-Print HintDb typeclass_instances.
-Print Scopes.
-*)
-
- Fixpoint gen_phiPOS1 (p:positive) : R :=
-  match p with
-  | xH => 1
-  | xO p => (1 + 1) * (gen_phiPOS1 p)
-  | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
-  end.
-
- Fixpoint gen_phiPOS (p:positive) : R :=
-  match p with
-  | xH => 1
-  | xO xH => (1 + 1)
-  | xO p => (1 + 1) * (gen_phiPOS p)
-  | xI xH => 1 + (1 +1)
-  | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
-  end.
-
- Definition gen_phiZ1 z :=
-  match z with
-  | Zpos p => gen_phiPOS1 p
-  | Z0 => 0
-  | Zneg p => -(gen_phiPOS1 p)
-  end.
-
- Definition gen_phiZ z :=
-  match z with
-  | Zpos p => gen_phiPOS p
-  | Z0 => 0
-  | Zneg p => -(gen_phiPOS p)
-  end.
- Notation "[ x ]" := (gen_phiZ x).
-
- Definition get_signZ z :=
-  match z with
-  | Zneg p => Some (Zpos p)
-  | _ => None
-  end.
-
-   Ltac norm := gen_cring_rewrite.
-   Ltac add_push :=  gen_add_push.
-Ltac rsimpl := simpl;  set_cring_notations.
-
- Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
- Proof.
-  induction x;rsimpl.
-  cring_rewrite IHx. destruct x;simpl;norm.
-  cring_rewrite IHx;destruct x;simpl;norm.
-  gen_reflexivity.
- Qed.
-
- Lemma ARgen_phiPOS_Psucc : forall x,
-   gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
- Proof.
-  induction x;rsimpl;norm.
-  cring_rewrite IHx ;norm.
-  add_push 1;gen_reflexivity.
- Qed.
-
- Lemma ARgen_phiPOS_add : forall x y,
-   gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
- Proof.
-  induction x;destruct y;simpl;norm.
-  cring_rewrite Pplus_carry_spec.
-  cring_rewrite ARgen_phiPOS_Psucc.
-  cring_rewrite IHx;norm.
-  add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity.
-  cring_rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity.
-  cring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
-  cring_rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity.
-  cring_rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity.
-  add_push 1;gen_reflexivity.
-  cring_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.
-  cring_rewrite ARgen_phiPOS_add;simpl;cring_rewrite IHx;norm.
-  cring_rewrite IHx;gen_reflexivity.
- Qed.
-
-
-(*morphisms are extensionaly equal*)
- Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
- Proof.
-  destruct x;rsimpl; try cring_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.
-  cring_rewrite H1;gen_reflexivity.
- Qed.
-
- Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1 (Z.pos_sub x y)
- == gen_phiPOS1 x + -gen_phiPOS1 y.
- Proof.
-  intros x y.
-  rewrite Z.pos_sub_spec.
-  assert (H0 := Pminus_mask_Gt x y). unfold Pgt in H0.
-  assert (H1 := Pminus_mask_Gt y x). unfold Pgt in H1.
-  rewrite Pos.compare_antisym in H1.
-  destruct (Pos.compare_spec x y) as [H|H|H].
-  subst. cring_rewrite cring_opp_def;gen_reflexivity.
-  destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; cring_rewrite Heq1;rewrite <- Heq2.
-  cring_rewrite ARgen_phiPOS_add;simpl;norm.
-  cring_rewrite cring_opp_def;norm.
-  destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
-  cring_rewrite ARgen_phiPOS_add;simpl;norm.
-  set_cring_notations. add_push (gen_phiPOS1 h). cring_rewrite cring_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.
- Proof. destruct x;simpl;intros;trivial. Qed.
-
- Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
- Proof.
-  intros x y; repeat cring_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.
-  cring_rewrite cring_add_comm. norm.
-  cring_rewrite ARgen_phiPOS_add; norm.
- Qed.
-
-Lemma gen_phiZ_opp : forall x, [- x] == - [x].
- Proof.
-  intros x. repeat cring_rewrite same_genZ. generalize x ;clear x.
-  induction x;simpl;norm.
-  cring_rewrite cring_opp_opp.  gen_reflexivity.
- Qed.
-
- Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
- Proof.
-  intros x y;repeat cring_rewrite same_genZ.
-  destruct x;destruct y;simpl;norm;
-  cring_rewrite  ARgen_phiPOS_mult;try (norm;fail).
-  cring_rewrite cring_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 : @Cring_morphism Z R Zr Rr.
- apply (Build_Cring_morphism Zr Rr gen_phiZ);simpl;try gen_reflexivity.
-   apply gen_phiZ_add. intros. cring_rewrite cring_sub_def. 
-replace (x-y)%Z with (x + (-y))%Z. cring_rewrite gen_phiZ_add. 
-cring_rewrite gen_phiZ_opp. gen_reflexivity.
-reflexivity.
- apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. 
- Defined.
-
-End ZMORPHISM.
-
-
-
-
diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
deleted file mode 100644
index f7e1a284d..000000000
--- a/plugins/setoid_ring/Cring_tac.v
+++ /dev/null
@@ -1,272 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import List.
-Require Import Setoid.
-Require Import BinPos.
-Require Import BinList.
-Require Import Znumtheory.
-Require Export Morphisms Setoid Bool.
-Require Import ZArith.
-Open Scope Z_scope.
-Require Import Algebra_syntax.
-Require Import Ring_polynom.
-Require Export Cring.
-Require Import Cring_initial.
-
-
-Set Implicit Arguments.
-
-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).
-
-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.
-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:Cring R) lvar 
- : reifyPE (PEc 0%Z) lvar cring0.
-Instance  reify_one (R:Type) (RR:Cring R) lvar 
- : reifyPE (PEc 1%Z) lvar cring1.
-Instance  reify_plus (R:Type)  (RR:Cring R)
-  e1 lvar t1 e2 t2 
- `{reifyPE R e1 lvar t1} 
- `{reifyPE R e2 lvar t2} 
- : reifyPE (PEadd e1 e2) lvar (cring_plus t1 t2).
-Instance  reify_mult (R:Type)  (RR:Cring R)
-  e1 lvar t1 e2 t2 
- `{reifyPE R e1 lvar t1} 
- `{reifyPE R e2 lvar t2}
- : reifyPE (PEmul e1 e2) lvar (cring_mult t1 t2).
-Instance  reify_sub (R:Type) (RR:Cring R) 
- e1 lvar t1 e2 t2 
- `{reifyPE R e1 lvar t1} 
- `{reifyPE R e2 lvar t2}
- : reifyPE (PEsub e1 e2) lvar (cring_sub t1 t2).
-Instance  reify_opp (R:Type) (RR:Cring R) 
- e1 lvar t1 
- `{reifyPE R e1 lvar t1}
- : reifyPE (PEopp e1) lvar (cring_opp t1).
-Instance  reify_pow (R:Type) (RR:Cring R) 
- e1 lvar t1 n 
- `{reifyPE R e1 lvar t1}
- : reifyPE (PEpow e1 n) lvar (@Ring_theory.pow_N _ cring1 cring_mult t1 n).
-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 
- | 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).
-
-Definition list_reifyl (R:Type) lexpr lvar lterm 
- `{reifyPElist R lexpr lvar lterm}
- `{is_closed_list (T:=R) lvar} := (lvar,lexpr).
-
-Unset Implicit Arguments.
-
-Instance multiplication_phi_cring{R:Type}{Rr:Cring R} : Multiplication  :=
-  {multiplication x y := cring_mult
-    (@gen_phiZ R Rr x) y}.
-
-(*
-Print HintDb typeclass_instances.
-*)
-(* Reification *)
-
-Ltac lterm_goal g :=
-  match g with
-  cring_eq ?t1 ?t2 => constr:(t1::t2::nil)
-  | cring_eq ?t1 ?t2 -> ?g => let lvar := lterm_goal g in constr:(t1::t2::lvar)     
-  end.
-
-Ltac reify_goal lvar lexpr 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 _ 0 addition multiplication subtraction opposite  Z
-               (@gen_phiZ _ _)
-               N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e); 
-           clear x;
-           reify_goal lvar lexpr1 lterm1
-        end
-  end.
-
-Existing Instance gen_phiZ_morph.
-Existing Instance Zr.
-
-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. 
-
-
-Lemma cring_eq_ext: forall (R:Type)(Rr:Cring R),
-  ring_eq_ext addition multiplication opposite cring_eq.
-intros. apply mk_reqe; set_cring_notations;intros. 
-cring_rewrite H0. cring_rewrite H. rrefl.
-cring_rewrite H0. cring_rewrite H. rrefl.
- cring_rewrite H. rrefl. Defined.
-
-Lemma cring_almost_ring_theory: forall (R:Type)(Rr:Cring R),
-   almost_ring_theory 0 1 addition multiplication subtraction opposite cring_eq.
-intros. apply mk_art ; set_cring_notations;intros.
-cring_rewrite cring_add_0_l; rrefl. 
-cring_rewrite cring_add_comm; rrefl. 
-cring_rewrite cring_add_assoc; rrefl. 
-cring_rewrite cring_mul_1_l; rrefl. 
-apply cring_mul_0_l.
-cring_rewrite cring_mul_comm; rrefl. 
-cring_rewrite cring_mul_assoc; rrefl. 
-cring_rewrite cring_distr_l; rrefl. 
-cring_rewrite cring_opp_mul_l; rrefl. 
-apply cring_opp_add.
-cring_rewrite cring_sub_def ; rrefl. Defined.
-
-Lemma cring_morph:  forall (R:Type)(Rr:Cring R),
-  ring_morph  0 1 addition multiplication subtraction opposite cring_eq
-             0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
-             (@gen_phiZ _ _).
-intros. apply mkmorph ; intros; simpl; try rrefl; set_cring_notations.
-cring_rewrite gen_phiZ_add; rrefl.
-cring_rewrite cring_sub_def. unfold Zminus. cring_rewrite gen_phiZ_add.
-cring_rewrite gen_phiZ_opp; rrefl.
-cring_rewrite gen_phiZ_mul; rrefl.
-cring_rewrite gen_phiZ_opp; rrefl.
-rewrite (Zeqb_ok x y H). rrefl. Defined.
-
-Lemma cring_power_theory :  forall (R:Type)(Rr:Cring R),
-  power_theory 1 (@multiplication _ _ (@multiplication_cring R Rr)) cring_eq (fun n:N => n)
-  (@Ring_theory.pow_N _  1 multiplication).
-intros; apply mkpow_th; set_cring_notations. rrefl. Defined.
-
-Lemma cring_div_theory: forall (R:Type)(Rr:Cring R),
-  div_theory cring_eq Zplus Zmult (gen_phiZ Rr) Z.quotrem.
-intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
-simpl.   apply (@cring_setoid R Rr). Defined.
-
-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; 
-           *)
-            let lv := fresh "lvar" in
-              set (lv := fv);
-                reify_goal lv lexpr lterm;
-                match goal with 
-                  |- ?g => 
-                    set_cring_notations ; unfold lv;
-                      generalize (@ring_correct _ 0 1 addition multiplication subtraction opposite 
-                        cring_eq
-                        cring_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 _ _) Z.quotrem (@cring_div_theory _ _) O fv nil);
-                      set_cring_notations;
-                      let rc := fresh "rc"in
-                        intro rc; apply rc
-                end
-        end
-  end.
-
-Ltac cring_compute:= vm_compute; reflexivity.
-
-Ltac cring:= 
-  unset_cring_notations; intros;
-  unfold multiplication_phi_cring; simpl gen_phiZ;
-  match goal with
-    |- (@cring_eq ?r ?rd _ _ ) =>
-          cring_gen; cring_compute
-  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.
-
-(* Tests *)
-
-Variable R: Type.
-Variable Rr: Cring R.
-Existing Instance Rr.
-
-Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
-cring.
-Qed.
-
-(* reification: 0,7s
-sinon, le reste de la tactique donne le même temps que ring 
-*)
-Goal forall x y z  t u :R, (x + y + z + t + u)^13 == (u + t + z + y + x) ^13.
-(*Time*) cring. (*Finished transaction in 0. secs (0.410938u,0.s)*)
-Qed.
-(*
-Goal forall x y z  t u :R, (x + y + z + t + u)^16 == (u + t + z + y + x) ^16.
-Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*)
-Qed.
-*)
-(*
-Require Export Ring.
-Open Scope Z_scope.
-Goal forall x y z  t u :Z, (x + y + z + t + u)^13 = (u + t + z + y + x) ^13.
-intros.
-Time ring.(*Finished transaction in 0. secs (0.371944u,0.s)*)
-Qed.
-
-Goal forall x y z  t u :Z, (x + y + z + t + u)^16 = (u + t + z + y + x) ^16.
-intros.
-Time ring.(*Finished transaction in 1. secs (0.914861u,0.s)*)
-Qed.
-*)
-
-Goal forall x y z:R, 6*x^2 + y  == y + 3*2*x^2 + 0 .
-cring.
-Qed.
-
-(*
-Goal forall x y z:R, x + y  == y + x + 0 .
-cring.
-Qed.
-
-Goal forall x y z:R, x * y * z == x * (y * z).
-cring.
-Qed.
-
-Goal forall x y z:R, 3 * x * (2%Z * y * z) == 6 * (x * y) * z.
-cring.
-Qed.
-
-Goal forall x y z:R, x ^ 2%N == x * x.
-cring.
-Qed.
-*)
-
-End Tests.
\ No newline at end of file
diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ncring.v
index bf65e8384..5b6987d01 100644
--- a/plugins/setoid_ring/Ring2.v
+++ b/plugins/setoid_ring/Ncring.v
@@ -12,7 +12,7 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import BinNat.
 Require Export Morphisms Setoid Bool.
-Require Export ZArith.
+Require Export ZArith_base.
 Require Export Algebra_syntax.
 
 Set Implicit Arguments.
@@ -26,14 +26,13 @@ Class Ring_ops(T:Type)
    {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.
+Instance zero_notation(T:Type)`{Ring_ops T}:Zero T:= ring0. 
+Instance one_notation(T:Type)`{Ring_ops T}:One T:= ring1.
+Instance add_notation(T:Type)`{Ring_ops T}:Addition T:= add.
+Instance mul_notation(T:Type)`{Ring_ops T}:@Multiplication T T:= mul.
+Instance sub_notation(T:Type)`{Ring_ops T}:Subtraction T:= sub.
+Instance opp_notation(T:Type)`{Ring_ops T}:Opposite T:= opp.
+Instance eq_notation(T:Type)`{Ring_ops T}:@Equality T:= ring_eq.
 
 Class Ring `{Ro:Ring_ops}:={
  ring_setoid: Equivalence _==_;
@@ -52,10 +51,10 @@ Class Ring `{Ro:Ring_ops}:={
  ring_sub_def    : \/x y, x - y == x + -y;
  ring_opp_def    : \/x, x + -x == 0
 }.
-
+(* inutile! je sais plus pourquoi j'ai mis ca...
 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.
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 21b86ff37..3c79f7d9b 100644
--- a/plugins/setoid_ring/Ring2_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -16,8 +16,8 @@ Require Import BinPos.
 Require Import BinNat.
 Require Import BinInt.
 Require Import Setoid.
-Require Export Ring2.
-Require Export Ring2_polynom.
+Require Export Ncring.
+Require Export Ncring_polynom.
 Import List.
 
 Set Implicit Arguments.
@@ -90,7 +90,7 @@ Context {R:Type}`{Ring R}.
   end.
 
    Ltac norm := gen_rewrite.
-   Ltac add_push :=  gen_add_push.
+   Ltac add_push :=  Ncring.gen_add_push.
 Ltac rsimpl := simpl.
 
  Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
@@ -98,15 +98,14 @@ Ltac rsimpl := simpl.
   induction x;rsimpl.
   rewrite IHx. destruct x;simpl;norm.
   rewrite IHx;destruct x;simpl;norm.
-  gen_reflexivity.
+  reflexivity.
  Qed.
 
  Lemma ARgen_phiPOS_Psucc : forall x,
    gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
  Proof.
   induction x;rsimpl;norm.
-  rewrite IHx ;norm.
-  add_push 1;gen_reflexivity.
+ rewrite IHx. gen_rewrite. add_push 1. reflexivity.
  Qed.
 
  Lemma ARgen_phiPOS_add : forall x y,
@@ -116,13 +115,13 @@ Ltac rsimpl := simpl.
   rewrite Pplus_carry_spec.
   rewrite ARgen_phiPOS_Psucc.
   rewrite IHx;norm.
-  add_push (gen_phiPOS1 y);add_push 1;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.
-  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+  add_push (gen_phiPOS1 y);add_push 1;reflexivity.
+  rewrite IHx;norm;add_push (gen_phiPOS1 y);reflexivity.
+  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity.
+  rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;reflexivity.
+  rewrite IHx;norm;add_push(gen_phiPOS1 y);reflexivity.
+  add_push 1;reflexivity.
+  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;reflexivity.
  Qed.
 
  Lemma ARgen_phiPOS_mult :
@@ -130,14 +129,14 @@ Ltac rsimpl := simpl.
  Proof.
   induction x;intros;simpl;norm.
   rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
-  rewrite IHx;gen_reflexivity.
+  rewrite IHx;reflexivity.
  Qed.
 
 
 (*morphisms are extensionaly equal*)
  Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
  Proof.
-  destruct x;rsimpl; try rewrite same_gen; gen_reflexivity.
+  destruct x;rsimpl; try rewrite same_gen; reflexivity.
  Qed.
 
  Lemma gen_Zeqb_ok : forall x y,
@@ -145,7 +144,7 @@ Ltac rsimpl := simpl.
  Proof.
   intros x y H7.
   assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10.
-  rewrite H10;gen_reflexivity.
+  rewrite H10;reflexivity.
  Qed.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
@@ -158,7 +157,7 @@ Ltac rsimpl := simpl.
   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.
+  subst. rewrite ring_opp_def;reflexivity.
   destruct HH1 as [h [HHeq1 [HHeq2 HHor]]];trivial.
   unfold Pminus; rewrite HHeq1;rewrite <- HHeq2.
   rewrite ARgen_phiPOS_add;simpl;norm.
@@ -168,38 +167,7 @@ Ltac rsimpl := simpl.
   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.
@@ -220,7 +188,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x].
  Proof.
   intros x. repeat rewrite same_genZ. generalize x ;clear x.
   induction x;simpl;norm.
-  rewrite ring_opp_opp.  gen_reflexivity.
+  rewrite ring_opp_opp.  reflexivity.
  Qed.
 
  Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
@@ -228,19 +196,19 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x].
   intros x y;repeat rewrite same_genZ.
   destruct x;destruct y;simpl;norm;
   rewrite  ARgen_phiPOS_mult;try (norm;fail).
-  rewrite ring_opp_opp ;gen_reflexivity.
+  rewrite ring_opp_opp ;reflexivity.
  Qed.
 
  Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
- Proof. intros;subst;gen_reflexivity. Qed.
+ Proof. intros;subst;reflexivity. Qed.
 
 (*proof that [.] satisfies morphism specifications*)
 Global Instance gen_phiZ_morph :
 (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
- apply Build_Ring_morphism; simpl;try gen_reflexivity.
+ apply Build_Ring_morphism; simpl;try 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.
+rewrite gen_phiZ_opp.  rewrite ring_sub_def. reflexivity.
 reflexivity.
  apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. 
  Defined.
diff --git a/plugins/setoid_ring/Ring2_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 969220e89..a3e14b30f 100644
--- a/plugins/setoid_ring/Ring2_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -15,7 +15,7 @@ Require Import BinPos.
 Require Import BinNat.
 Require Import BinInt.
 Require Export Ring_polynom. (* n'utilise que PExpr *)
-Require Export Ring2.
+Require Export Ncring.
 
 Section MakeRingPol.
 
@@ -618,5 +618,4 @@ exact pow_th.
   apply Peq_ok;trivial.
  Qed.
 
-
 End MakeRingPol.
\ No newline at end of file
diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ncring_tac.v
index fad36e571..34731eb3b 100644
--- a/plugins/setoid_ring/Ring2_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -14,9 +14,9 @@ Require Import Znumtheory.
 Require Export Morphisms Setoid Bool.
 Require Import ZArith.
 Require Import Algebra_syntax.
-Require Export Ring2.
-Require Import Ring2_polynom.
-Require Import Ring2_initial.
+Require Export Ncring.
+Require Import Ncring_polynom.
+Require Import Ncring_initial.
 
 
 Set Implicit Arguments.
@@ -49,6 +49,18 @@ Instance  reify_one (R:Type)  lvar op
  `{Ring (T:=R)(ring1:=op)}
  : reify (ring1:=op) (PEc 1%Z) lvar op.
 
+Instance  reifyZ0 (R:Type)  lvar 
+ `{Ring (T:=R)}
+ : reify (PEc Z0) lvar Z0|11.
+
+Instance  reifyZpos (R:Type)  lvar (p:positive)
+ `{Ring (T:=R)}
+ : reify (PEc (Zpos p)) lvar (Zpos p)|11.
+
+Instance  reifyZneg (R:Type)  lvar (p:positive)
+ `{Ring (T:=R)}
+ : reify (PEc (Zneg p)) lvar (Zneg p)|11.
+
 Instance  reify_add (R:Type)
   e1 lvar t1 e2 t2 op 
  `{Ring (T:=R)(add:=op)}
@@ -61,7 +73,7 @@ Instance  reify_mul (R:Type)
  `{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).
+ : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
 
 Instance  reify_mul_ext (R:Type) `{Ring R}
   lvar z e2 t2 
@@ -120,6 +132,7 @@ Ltac lterm_goal g :=
   match g with
   | ?t1 == ?t2 => constr:(t1::t2::nil)
   | ?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.
@@ -140,7 +153,7 @@ Ltac reify_goal lvar lexpr lterm:=
                       (fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
                       lvar e2))
         end
-  end.
+  end. 
 
 Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R),
   x * (gen_phiZ c) == (gen_phiZ c) * x.
@@ -177,7 +190,119 @@ Ltac ring_gen :=
        end
    end.
 
-Ltac ring2:= 
+Ltac non_commutative_ring:= 
   intros;
   ring_gen.
 
+(* simplification *)
+
+Ltac ring_simplify_aux lterm fv lexpr hyp :=
+    match lterm with
+      | ?t0::?lterm =>
+    match lexpr with
+      | ?e::?le => (* e:PExpr Z est la réification de t0:R *)
+        let t := constr:(@Ncring_polynom.norm_subst
+          Z 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z) Zops Zeq_bool e) in
+        (* t:Pol Z *)
+        let te := 
+          constr:(@Ncring_polynom.Pphi Z 
+            _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ fv t) in
+        let eq1 := fresh "ring" in
+        let nft := eval vm_compute in t in
+        let t':= fresh "t" in
+        pose (t' := nft);
+        assert (eq1 : t = t');
+        [vm_cast_no_check (refl_equal t')|
+        let eq2 := fresh "ring" in
+        assert (eq2:(@Ncring_polynom.PEeval Z
+          _ 0 1 _+_ _*_ _-_ -_ _==_ _ Ncring_initial.gen_phiZ N (fun n:N => n) 
+          (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
+        [apply (@Ncring_polynom.norm_subst_ok
+          Z _ 0%Z 1%Z Zplus Zmult Zminus Zopp (@eq Z)
+          _ _ 0 1 _+_ _*_ _-_ -_ _==_ _ _ Ncring_initial.gen_phiZ _
+          (@comm _ 0 1 _+_ _*_ _-_ -_ _==_ _ _) _ Zeqb_ok);
+           apply mkpow_th; reflexivity
+          | match hyp with
+                | 1%nat => rewrite eq2
+                | ?H => try rewrite eq2 in H
+              end];
+        let P:= fresh "P" in
+        match hyp with
+          | 1%nat => idtac "ok";
+            rewrite eq1;
+            pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_
+              _ Ncring_initial.gen_phiZ fv t');
+            match goal with
+              |- (?p ?t) => set (P:=p)
+            end;
+              unfold t' in *; clear t' eq1 eq2; simpl
+          | ?H =>
+               rewrite eq1 in H;
+               pattern (@Ncring_polynom.Pphi Z _ 0 1 _+_ _*_ _-_ -_ _==_
+                  _ Ncring_initial.gen_phiZ fv t') in H; 
+               match type of H with
+                  | (?p ?t)  => set (P:=p) in H
+               end;
+               unfold t' in *; clear t' eq1 eq2; simpl in H
+        end; unfold P in *; clear P
+        ]; ring_simplify_aux lterm fv le hyp
+      | nil => idtac
+    end
+    | nil => idtac
+    end.
+
+Ltac set_variables fv :=
+  match fv with
+    | nil => idtac
+    | ?t::?fv =>
+        let v := fresh "X" in
+        set (v:=t) in *; set_variables fv
+  end.
+
+Ltac deset n:=
+   match n with
+    | 0%nat => idtac
+    | S ?n1 =>
+      match goal with
+        | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
+      end
+   end.
+
+(* a est soit un terme de l'anneau, soit une liste de termes.
+J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list
+ dans Tactic Notation *)
+
+Ltac ring_simplify_gen a hyp :=
+  let lterm :=
+    match a with
+      | _::_ => a
+      | _ => constr:(a::nil)
+    end in
+    match eval red in (list_reifyl (lterm:=lterm)) with
+      | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
+      let n := eval compute in (length fv) in
+      idtac n;
+      let lt:=fresh "lt" in
+      set (lt:= lterm);
+      let lv:=fresh "fv" in
+      set (lv:= fv);
+      (* les termes de fv sont remplacés par des variables 
+         pour pouvoir utiliser simpl ensuite sans risquer
+         des simplifications indésirables *)
+      set_variables fv;
+      let lterm1 := eval unfold lt in lt in
+      let lv1 := eval unfold lv in lv in
+        idtac lterm1; idtac lv1;
+      ring_simplify_aux lterm1 lv1 lexpr hyp;
+      clear lt lv;
+      (* on remet les termes de fv *)
+      deset n
+    end.
+
+Tactic Notation "non_commutative_ring_simplify" constr(lterm):=
+ ring_simplify_gen lterm 1%nat.
+
+Tactic Notation "non_commutative_ring_simplify" constr(lterm) "in" ident(H):=
+ ring_simplify_gen lterm H.
+
+
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 2b08f9400..4297e3a8b 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -15,7 +15,10 @@ Ring.vo
 ZArithRing.vo
 Algebra_syntax.vo
 Cring.vo
-Ring2.vo
-Ring2_polynom.vo
-Ring2_initial.vo
-Ring2_tac.vo
\ No newline at end of file
+Ncring.vo
+Ncring_polynom.vo
+Ncring_initial.vo
+Ncring_tac.vo
+Cring_R.vo
+Cring_Q.vo
+Integral_domain.vo
\ No newline at end of file