Imported Upstream version 8.4~betaupstream/8.4_beta

24 files changed, 2045 insertions, 233 deletions

diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
new file mode 100644
index 00000000..e896554e
--- /dev/null
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -0,0 +1,25 @@
+
+Class Zero (A : Type) := zero : A.
+Notation "0" := zero.
+Class One (A : Type) := one : A.
+Notation "1" := one.
+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.
+Notation "_*_" := multiplication.
+Notation "x * y" := (multiplication x y).
+Class Subtraction (A : Type) := subtraction : A -> A -> A.
+Notation "_-_" := subtraction.
+Notation "x - y" := (subtraction x y).
+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).
+
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 6998b656..06822ae1 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -21,12 +21,12 @@ Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
 
 Lemma nat_morph_N :
    semi_morph 0 1 plus mult (eq (A:=nat))
-          0%N 1%N Nplus Nmult Neq_bool nat_of_N.
+          0%N 1%N N.add N.mul N.eqb nat_of_N.
 Proof.
   constructor;trivial.
   exact nat_of_Nplus.
   exact nat_of_Nmult.
-  intros x y H;rewrite (Neq_bool_ok _ _ H);trivial.
+  intros x y H. apply N.eqb_eq in H. now subst.
 Qed.
 
 Ltac natcst t :=
diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v
index 905625cc..7128280a 100644
--- a/plugins/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
new file mode 100644
index 00000000..3d6e53fc
--- /dev/null
+++ b/plugins/setoid_ring/Cring.v
@@ -0,0 +1,272 @@
+(************************************************************************)
+(*  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 Export List.
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinList.
+Require Import Znumtheory.
+Require Export Morphisms Setoid Bool.
+Require Import ZArith_base.
+Require Export Algebra_syntax.
+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.
+
+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 Ncring_initial.gen_phiZ N (fun n:N => n)
+               (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
+             (@Ring_polynom.PEeval
+               _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
+               (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
+        end
+  end.
+
+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
+             Ncring_initial.gen_phiZ.
+intros. apply mkmorph ; intros; simpl; try 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 : 
+  @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 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
+        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
+                        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
+                        O fv nil);
+                 let rc := fresh "rc"in
+                   intro rc; apply rc
+           end
+        end
+  end.
+
+Ltac cring_compute:= vm_compute; reflexivity.
+
+Ltac cring:= 
+  intros;
+  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/Field.v b/plugins/setoid_ring/Field.v
index 6a755af2..90f2f497 100644
--- a/plugins/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index eee89e61..da42bbd9 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index ccdec656..40138526 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -96,7 +96,7 @@ Hint Resolve (ARadd_0_l  ARth) (ARadd_comm  ARth) (ARadd_assoc ARth)
              (ARsub_def  ARth) .
 
  (* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.
  Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -390,52 +390,16 @@ Qed.
 
   ***************************************************************************)
 
-Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool :=
- match p1, p2 with
-   xH, xH => true
-  | xO p3, xO p4 => positive_eq p3 p4
-  | xI p3, xI p4 => positive_eq p3 p4
-  | _, _ => false
- end.
-
-Theorem positive_eq_correct:
- forall p1 p2,  if positive_eq p1 p2 then p1 = p2 else p1 <> p2.
-intros p1; elim p1;
- (try (intros p2; case p2; simpl; auto; intros; discriminate)).
-intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
-generalize (rec p4); case (positive_eq p3 p4); auto.
-intros H1; apply f_equal with ( f := xI ); auto.
-intros H1 H2; case H1; injection H2; auto.
-intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
-generalize (rec p4); case (positive_eq p3 p4); auto.
-intros H1; apply f_equal with ( f := xO ); auto.
-intros H1 H2; case H1; injection H2; auto.
-Qed.
-
-Definition N_eq n1 n2 :=
-  match n1, n2 with
-  | N0, N0 => true
-  | Npos p1, Npos p2 => positive_eq p1 p2
-  | _, _ => false
-  end.
-
-Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2.
-Proof.
-  intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail).
-  assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2);
-     [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial].
-Qed.
-
 (* equality test *)
 Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
  match e1, e2 with
    PEc c1, PEc c2 => ceqb c1 c2
-  | PEX p1, PEX p2 => positive_eq p1 p2
+  | PEX p1, PEX p2 => Pos.eqb p1 p2
   | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
   | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
   | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
   | PEopp e3, PEopp e4 => PExpr_eq e3 e4
-  | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false
+  | PEpow e3 n3, PEpow e4 n4 => if N.eqb n3 n4 then PExpr_eq e3 e4 else false
   | _, _ => false
  end.
 
@@ -460,8 +424,7 @@ intros l e1; elim e1.
 intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)).
 intros c2; apply (morph_eq CRmorph).
 intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)).
-intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2);
- (try (intros; discriminate)); intros H; rewrite H; auto.
+intros p2; case Pos.eqb_spec; intros; now subst.
 intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
 intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
  (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
@@ -478,9 +441,8 @@ intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))).
 intros e4; generalize (rec e4); case (PExpr_eq e3 e4);
  (try (intros; discriminate)); auto.
 intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))).
-intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4);
-intros;try discriminate.
-repeat rewrite  pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto.
+intros e4 n4; case N.eqb_spec; try discriminate; intros EQ H; subst.
+repeat rewrite  pow_th.(rpow_pow_N). rewrite (rec _ H);auto.
 Qed.
 
 (* add *)
@@ -507,7 +469,7 @@ Definition NPEpow x n :=
   match n with
   | N0 => PEc cI
   | Npos p =>
-    if positive_eq p xH then x else
+    if Pos.eqb p xH then x else
     match x with
     | PEc c =>
       if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p)
@@ -520,10 +482,10 @@ Theorem NPEpow_correct : forall l e n,
 Proof.
  destruct n;simpl.
  rewrite pow_th.(rpow_pow_N);simpl;auto.
- generalize (positive_eq_correct p xH).
- destruct (positive_eq p 1);intros.
- rewrite H;rewrite  pow_th.(rpow_pow_N). trivial.
- clear H;destruct e;simpl;auto.
+ fold (p =? 1)%positive.
+ case Pos.eqb_spec; intros H; (rewrite H || clear H).
+ now rewrite  pow_th.(rpow_pow_N).
+ destruct e;simpl;auto.
  repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl.
  symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)].
  symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)].
@@ -539,7 +501,7 @@ Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C :=
   |  _, PEc c =>
       if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
   | PEpow e1 n1, PEpow e2 n2 =>
-      if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
+      if N.eqb n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y
   | _, _ => PEmul x y
   end.
 
@@ -554,10 +516,10 @@ induction e1;destruct e2; simpl in |- *;try reflexivity;
  try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity;
  try ring [(morph0 CRmorph) (morph1 CRmorph)].
  apply (morph_mul CRmorph).
-assert (H:=N_eq_correct n n0);destruct (N_eq n n0).
+case N.eqb_spec; intros H; try rewrite <- H; clear H.
 rewrite NPEpow_correct. simpl.
 repeat rewrite pow_th.(rpow_pow_N).
-rewrite IHe1;rewrite <- H;destruct n;simpl;try ring.
+rewrite IHe1; destruct n;simpl;try ring.
 apply pow_pos_mul.
 simpl;auto.
 Qed.
@@ -760,6 +722,14 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
  Notation pow_pos_plus :=  (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext)
                         ARth.(ARmul_comm) ARth.(ARmul_assoc)).
 
+ Lemma Z_pos_sub_gt : forall p q, (p > q)%positive ->
+  Z.pos_sub p q = Zpos (p - q).
+ Proof.
+  intros. apply Z.pos_sub_gt. now apply Pos.gt_lt.
+ Qed.
+
+ Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
+
  Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
   match
       (if  PExpr_eq e1 e2 then
@@ -779,10 +749,12 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
 Proof.
   intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
    case (PExpr_eq e1 e2); simpl; auto; intros H.
-  case_eq ((p1 ?= p2)%positive Eq);intros;simpl.
+  rewrite Z.pos_sub_spec.
+  case_eq ((p1 ?= p2)%positive);intros;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
   rewrite (Pcompare_Eq_eq _ _ H0).
   rewrite H by trivial. ring [ (morph1 CRmorph)].
+  fold (p2 - p1 =? 1)%positive.
   fold (NPEpow e2 (Npos (p2 - p1))).
   rewrite NPEpow_correct;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
@@ -790,22 +762,17 @@ Proof.
   rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
   rewrite H;trivial.
-   change (ZtoN
-     match (p1 ?= p1 - p2)%positive Eq with
-     | Eq => 0
-     | Lt => Zneg (p1 - p2 - p1)
-     | Gt => Zpos (p1 - (p1 - p2))
-     end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))).
+   change (Z.pos_sub p1 (p1-p2)) with (Zpos p1 - Zpos (p1 -p2))%Z.
   replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
   split.
   repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
-  rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl.
+  rewrite Zplus_assoc, Z.add_opp_diag_r. simpl.
   ring [ (morph1 CRmorph)].
  assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _).
  apply Zplus_gt_reg_l with (Zpos p2).
  rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
  apply Zplus_gt_compat_r. refine (refl_equal _).
- simpl;rewrite H0;trivial.
+ simpl. now simpl_pos_sub.
 Qed.
 
 Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
@@ -835,7 +802,7 @@ destruct n.
   destruct n;simpl.
     rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
     intros (H1,H2) (H3,H4).
-    unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
+    simpl_pos_sub. simpl in H3.
     rewrite pow_pos_mul. rewrite H1;rewrite H3.
     assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
         (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
@@ -845,11 +812,10 @@ destruct n.
    split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
    repeat rewrite pow_th.(rpow_pow_N);simpl.
    intros (H1,H2) (H3,H4).
-   unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
-   rewrite H2 in H1;simpl in H1.
+   simpl_pos_sub. simpl in H1, H3.
    assert (Zpos p1 > Zpos p6)%Z.
      apply Zgt_trans with (Zpos p4). exact H4. exact H2.
-  unfold Zgt in H;simpl in H;rewrite H.
+  simpl_pos_sub.
   split. 2:exact H.
   rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
   assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
@@ -863,11 +829,11 @@ destruct n.
      (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
  change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
  rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)).
- simpl. rewrite Pcompare_refl. simpl. reflexivity.
+ simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
  unfold Zminus, Zopp in H0. simpl in H0.
-  rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
+  simpl_pos_sub. inversion H0; trivial.
  simpl. repeat rewrite pow_th.(rpow_pow_N).
- intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3.
+ intros H1 (H2,H3). simpl_pos_sub.
  rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
  simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
  rewrite pow_pos_mul. split. ring [H2]. exact H3.
@@ -878,8 +844,7 @@ destruct n.
  rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
  repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
  intros (H1, H2);rewrite H1;split.
-   unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1.
-   simpl in H1;ring [H1]. trivial.
+   simpl_pos_sub. simpl in H1;ring [H1]. trivial.
  trivial.
  destruct n. trivial.
  generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
@@ -937,8 +902,7 @@ Proof.
      repeat rewrite NPEpow_correct;simpl;
      repeat rewrite pow_th.(rpow_pow_N);simpl).
   intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
-  intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H.
-  simpl in H;split;try ring [H].
+  intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
   rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
   simpl;intros. repeat rewrite NPEmul_correct;simpl.
   rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
@@ -1805,25 +1769,24 @@ Lemma gen_phiPOS_inj : forall x y,
   x = y.
 intros x y.
 repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
-ElimPcompare x y; intro.
+case (Pos.compare_spec x y).
+ intros.
+   trivial.
  intros.
-   apply Pcompare_Eq_eq; trivial.
- intro.
    elim gen_phiPOS_not_0 with (y - x)%positive.
    apply add_inj_r with x.
    symmetry  in |- *.
    rewrite (ARadd_0_r Rsth ARth) in |- *.
    rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
    rewrite Pplus_minus in |- *; trivial.
-   change Eq with (CompOpp Eq) in |- *.
-   rewrite <- Pcompare_antisym in |- *; trivial.
-   rewrite H in |- *; trivial.
- intro.
+   now apply Pos.lt_gt.
+ intros.
    elim gen_phiPOS_not_0 with (x - y)%positive.
    apply add_inj_r with y.
    rewrite (ARadd_0_r Rsth ARth) in |- *.
    rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
    rewrite Pplus_minus in |- *; trivial.
+   now apply Pos.lt_gt.
 Qed.
 
 
@@ -1841,12 +1804,9 @@ Qed.
 
 Lemma gen_phiN_complete : forall x y,
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
-  Neq_bool x y = true.
-intros.
- replace y with x.
- unfold Neq_bool in |- *.
-   rewrite Ncompare_refl in |- *; trivial.
- apply gen_phiN_inj; trivial.
+  N.eqb x y = true.
+Proof.
+intros. now apply N.eqb_eq, gen_phiN_inj.
 Qed.
 
 End AlmostField.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 026e70c8..763dbe7b 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -13,7 +13,6 @@ Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_polynom.
-Require Import ZOdiv_def.
 Import List.
 
 Set Implicit Arguments.
@@ -170,48 +169,28 @@ Section ZMORPHISM.
   rewrite H1;rrefl.
  Qed.
 
- Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive Eq with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
- == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Lemma gen_phiZ1_pos_sub : forall x y,
+ gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
-  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
-  generalize (Pminus_mask_Gt y x).
-  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
-  rewrite <- Pcompare_antisym in H1.
-  destruct ((x ?= y)%positive Eq).
-  rewrite H;trivial. rewrite (Ropp_def Rth);rrefl.
-  destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+  rewrite Z.pos_sub_spec.
+  case Pos.compare_spec; intros H; simpl.
+  rewrite H. rewrite (Ropp_def Rth);rrefl.
+  rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
   rewrite (ARgen_phiPOS_add ARth);simpl;norm.
   rewrite (Ropp_def Rth);norm.
-  destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
-  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+  rewrite <- (Pos.sub_add x y H) at 2.
   rewrite (ARgen_phiPOS_add ARth);simpl;norm.
-  add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm.
+  add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); 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 rewrite same_genZ; generalize x y;clear x y.
-  induction x;destruct y;simpl;norm.
+  destruct x, y; simpl; norm.
   apply (ARgen_phiPOS_add ARth).
-  apply gen_phiZ1_add_pos_neg.
-  replace Eq with (CompOpp Eq);trivial.
-  rewrite <- Pcompare_antisym;simpl.
-  rewrite match_compOpp.
-  rewrite (Radd_comm Rth).
-  apply gen_phiZ1_add_pos_neg.
+  apply gen_phiZ1_pos_sub.
+  rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
   rewrite (ARgen_phiPOS_add ARth); norm.
  Qed.
 
@@ -244,47 +223,28 @@ End ZMORPHISM.
 Lemma Nsth : Setoid_Theory N (@eq N).
 Proof (Eqsth N).
 
-Lemma Nseqe : sring_eq_ext Nplus Nmult (@eq N).
-Proof (Eq_s_ext Nplus Nmult).
+Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).
+Proof (Eq_s_ext N.add N.mul).
 
-Lemma Nth : semi_ring_theory N0 (Npos xH) Nplus Nmult (@eq N).
+Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
 Proof.
- constructor. exact Nplus_0_l. exact Nplus_comm. exact Nplus_assoc.
- exact Nmult_1_l. exact Nmult_0_l. exact Nmult_comm. exact Nmult_assoc.
- exact Nmult_plus_distr_r.
+ constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
+ exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
+ exact N.mul_add_distr_r.
 Qed.
 
-Definition Nsub := SRsub Nplus.
+Definition Nsub := SRsub N.add.
 Definition Nopp := (@SRopp N).
 
-Lemma Neqe : ring_eq_ext Nplus Nmult Nopp (@eq N).
+Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
 Proof (SReqe_Reqe Nseqe).
 
 Lemma Nath :
- almost_ring_theory N0 (Npos xH) Nplus Nmult Nsub Nopp (@eq N).
+ almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
 Proof (SRth_ARth Nsth Nth).
 
-Definition Neq_bool (x y:N) :=
-  match Ncompare x y with
-  | Eq => true
-  | _ => false
-  end.
-
-Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y.
- Proof.
-  intros x y;unfold Neq_bool.
-  assert (H:=Ncompare_Eq_eq x y);
-   destruct (Ncompare x y);intros;try discriminate.
-  rewrite H;trivial.
- Qed.
-
-Lemma Neq_bool_complete : forall x y, Neq_bool x y = true -> x = y.
- Proof.
-  intros x y;unfold Neq_bool.
-  assert (H:=Ncompare_Eq_eq x y);
-   destruct (Ncompare x y);intros;try discriminate.
-  rewrite H;trivial.
- Qed.
+Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
+Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
 
 (**Same as above : definition of two,extensionaly equal, generic morphisms *)
 (**from N to any semi-ring*)
@@ -307,9 +267,7 @@ Section NMORPHISM.
   Notation "x == y" := (req x y).
    Add Morphism radd : radd_ext4.  exact (Radd_ext Reqe). Qed.
    Add Morphism rmul : rmul_ext4.  exact (Rmul_ext Reqe). Qed.
-   Add Morphism ropp : ropp_ext4.  exact (Ropp_ext Reqe). Qed.
-   Add Morphism rsub : rsub_ext5.  exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite Rsth Reqe ARth.
+   Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
 
  Definition gen_phiN1 x :=
   match x with
@@ -326,8 +284,8 @@ Section NMORPHISM.
 
  Lemma same_genN : forall x, [x] == gen_phiN1 x.
  Proof.
-  destruct x;simpl. rrefl.
-  rewrite (same_gen Rsth Reqe ARth);rrefl.
+  destruct x;simpl. reflexivity.
+  now rewrite (same_gen Rsth Reqe ARth).
  Qed.
 
  Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].
@@ -349,11 +307,11 @@ Section NMORPHISM.
 
 (*gen_phiN satisfies morphism specifications*)
  Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
-                           N0 (Npos xH) Nplus Nmult Nsub Nopp Neq_bool gen_phiN.
+                           0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
  Proof.
-  constructor;intros;simpl; try rrefl.
-  apply gen_phiN_add. apply gen_phiN_sub.  apply gen_phiN_mult.
-  rewrite (Neq_bool_ok x y);trivial. rrefl.
+  constructor; simpl; try reflexivity.
+  apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
+  intros x y EQ. apply N.eqb_eq in EQ. now subst.
  Qed.
 
 End NMORPHISM.
@@ -402,7 +360,7 @@ Fixpoint Nw_is0 (w : Nword) : bool :=
 Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
   match w1, w2 with
   | n1::w1', n2::w2' =>
-     if Neq_bool n1 n2 then Nweq_bool w1' w2' else false
+     if N.eqb n1 n2 then Nweq_bool w1' w2' else false
   | nil, _ => Nw_is0 w2
   | _, nil => Nw_is0 w1
   end.
@@ -486,10 +444,10 @@ induction w1; intros.
 
   simpl in H.
   rewrite gen_phiNword_cons in |- *.
-  case_eq (Neq_bool a n); intros.
+  case_eq (N.eqb a n); intros H0.
    rewrite H0 in H.
-   rewrite <- (Neq_bool_ok _ _ H0) in |- *.
-   rewrite (IHw1 _ H) in |- *.
+   apply N.eqb_eq in H0. rewrite <- H0.
+   rewrite (IHw1 _ H).
    reflexivity.
 
    rewrite H0 in H;  discriminate H.
@@ -632,19 +590,19 @@ Qed.
 
  Variable zphi : Z -> R.
 
- Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi ZOdiv_eucl.
+ Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
  Proof.
   constructor.
-  intros; generalize (ZOdiv_eucl_correct a b); case ZOdiv_eucl; intros; subst.
-  rewrite Zmult_comm; rsimpl.
+  intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
+  rewrite Z.mul_comm; rsimpl.
  Qed.
 
  Variable nphi : N -> R.
 
- Lemma Ntriv_div_th : div_theory req Nplus Nmult nphi Ndiv_eucl.
+ Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
   constructor.
-  intros; generalize (Ndiv_eucl_correct a b); case Ndiv_eucl; intros; subst.
-  rewrite Nmult_comm; rsimpl.
+  intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
+  rewrite N.mul_comm; rsimpl.
  Qed.
 
 End GEN_DIV.
diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v
new file mode 100644
index 00000000..5a224e38
--- /dev/null
+++ b/plugins/setoid_ring/Integral_domain.v
@@ -0,0 +1,44 @@
+Require Export Cring.
+
+
+(* 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.
+
+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.
+
+
+Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n).
+
+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. apply ring_setoid.
+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.   
+
+End integral_domain.
+
diff --git a/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 8d7cb0ea..fafd16ab 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -18,4 +18,4 @@ Ltac Ncst t :=
   | _ => constr:NotConstant
   end.
 
-Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).
+Add Ring Nr : Nth (decidable Neqb_ok, constants [Ncst]).
diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v
new file mode 100644
index 00000000..9a30fa47
--- /dev/null
+++ b/plugins/setoid_ring/Ncring.v
@@ -0,0 +1,305 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* non commutative rings *)
+
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinNat.
+Require Export Morphisms Setoid Bool.
+Require Export ZArith_base.
+Require Export Algebra_syntax.
+
+Set Implicit Arguments.
+
+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:= 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 _==_;
+ ring_plus_comp: Proper (_==_ ==> _==_ ==>_==_) _+_;
+ ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_;
+ ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_;
+ ring_opp_comp: Proper (_==_==>_==_) -_;
+ ring_add_0_l    : forall x, 0 + x == x;
+ ring_add_comm   : forall x y, x + y == y + x;
+ ring_add_assoc  : forall x y z, x + (y + z) == (x + y) + z;
+ ring_mul_1_l    : forall x, 1 * x == x;
+ ring_mul_1_r    : forall x, x * 1 == x;
+ ring_mul_assoc  : forall x y z, x * (y * z) == (x * y) * z;
+ ring_distr_l    : forall x y z, (x + y) * z == x * z + y * z;
+ ring_distr_r    : forall x y z, z * ( x + y) == z * x + z * y;
+ ring_sub_def    : forall x y, x - y == x + -y;
+ ring_opp_def    : forall 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.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
+
+Section Ring_power.
+
+Context {R:Type}`{Ring R}.
+
+ 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)
+  end.
+
+ 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 : forall x y, [x + y] == [x] + [y];
+    ring_morphism_sub : forall x y, [x - y] == [x] - [y];
+    ring_morphism_mul : forall x y, [x * y] == [x] * [y];
+    ring_morphism_opp : forall  x, [-x] == -[x];
+    ring_morphism_eq  : forall x y, x == y -> [x] == [y]}.
+
+Section Ring.
+
+Context {R:Type}`{Rr:Ring R}.
+
+(* Powers *)
+
+ Lemma pow_pos_comm : forall  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.
+ Proof.
+  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.
+reflexivity. reflexivity.
+Qed.
+
+ Lemma pow_pos_Pplus : forall  x i j,
+   pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+  intro x;induction i;intros.
+  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat rewrite IHi.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
+  rewrite pow_pos_Psucc.
+  simpl;repeat rewrite ring_mul_assoc. reflexivity.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat rewrite IHi. rewrite ring_mul_assoc. reflexivity.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc.
+   simpl. reflexivity. 
+ Qed.
+
+ 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; reflexivity.
+ Qed.
+
+ (** Identity is a morphism *)
+ (*
+ Instance IDmorph : Ring_morphism _ _ _  (fun x => x).
+ Proof.
+  apply (Build_Ring_morphism H6 H6 (fun x => x));intros;
+  try reflexivity. trivial.
+ Qed.
+*)
+ (** rings are almost rings*)
+ Lemma ring_mul_0_l : forall  x, 0 * x == 0.
+ Proof.
+  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.
+ Proof.
+  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.
+
+  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.
+ Proof.
+  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.
+ Proof.
+  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.
+ Proof.
+  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.
+ Proof.
+  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.
+ Proof.
+  intros.
+  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 mrewrite :=
+   repeat first
+     [ 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; mrewrite. Qed.
+
+ 
+ Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Proof.
+  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.
+ Proof.
+  intros; repeat rewrite <- ring_add_assoc.
+   rewrite (ring_add_comm x); reflexivity.
+ Qed.
+
+ Lemma ring_opp_zero : -0 == 0.
+ Proof.
+  rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l.
+  repeat rewrite ring_mul_0_r. reflexivity.
+ Qed.
+
+End Ring.
+
+(** Some simplification tactics*)
+Ltac gen_reflexivity := reflexivity.
+ 
+Ltac gen_rewrite :=
+  repeat first
+     [ 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 :=
+repeat (match goal with
+  | |- context [(?y + x) + ?z] =>
+     progress rewrite (ring_add_assoc2 x y z)
+  | |- context [(x + ?y) + ?z] =>
+     progress rewrite  (ring_add_assoc1 x y z)
+  end).
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
new file mode 100644
index 00000000..3c79f7d9
--- /dev/null
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -0,0 +1,221 @@
+(************************************************************************)
+(*  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 BinList.
+Require Import BinPos.
+Require Import BinNat.
+Require Import BinInt.
+Require Import Setoid.
+Require Export Ncring.
+Require Export Ncring_polynom.
+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.
+
+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.  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.
+Context {R:Type}`{Ring R}.
+
+ Ltac rrefl := reflexivity.
+
+ 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_rewrite.
+   Ltac add_push :=  Ncring.gen_add_push.
+Ltac rsimpl := simpl.
+
+ Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
+ Proof.
+  induction x;rsimpl.
+  rewrite IHx. destruct x;simpl;norm.
+  rewrite IHx;destruct x;simpl;norm.
+  reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_Psucc : forall x,
+   gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
+ Proof.
+  induction x;rsimpl;norm.
+ rewrite IHx. gen_rewrite. add_push 1. 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.
+  rewrite Pplus_carry_spec.
+  rewrite ARgen_phiPOS_Psucc.
+  rewrite IHx;norm.
+  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 :
+   forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
+ Proof.
+  induction x;intros;simpl;norm.
+  rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
+  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; reflexivity.
+ Qed.
+
+ Lemma gen_Zeqb_ok : forall x y,
+   Zeq_bool x y = true -> [x] == [y].
+ Proof.
+  intros x y H7.
+  assert (H10 := Zeq_bool_eq x y H7);unfold IDphi in H10.
+  rewrite H10;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 (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;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 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 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. 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 rewrite same_genZ. generalize x ;clear x.
+  induction x;simpl;norm.
+  rewrite ring_opp_opp.  reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
+ Proof.
+  intros x y;repeat rewrite same_genZ.
+  destruct x;destruct y;simpl;norm;
+  rewrite  ARgen_phiPOS_mult;try (norm;fail).
+  rewrite ring_opp_opp ;reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
+ 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 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. 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/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
new file mode 100644
index 00000000..c0d31587
--- /dev/null
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -0,0 +1,621 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*  A <X1,...,Xn>: non commutative polynomials on a commutative ring A *)
+
+Set Implicit Arguments.
+Require Import Setoid.
+Require Import BinList.
+Require Import BinPos.
+Require Import BinNat.
+Require Import BinInt.
+Require Export Ring_polynom. (* n'utilise que PExpr *)
+Require Export Ncring.
+
+Section MakeRingPol.
+
+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_rewrite || rewrite phiCR_comm).
+ Ltac add_push := gen_add_push .
+
+(* Definition of non commutative multivariable polynomials 
+   with coefficients in C :
+ *)
+
+ Inductive Pol : Type :=
+  | Pc : C -> Pol
+  | PX : Pol -> positive -> positive -> Pol -> Pol. 
+    (* PX P i n Q represents P * X_i^n + Q *)
+Definition cO:C . exact ring0. Defined.
+Definition cI:C . exact ring1. Defined.
+
+ Definition P0 := Pc 0.
+ Definition P1 := Pc 1.
+
+Variable Ceqb:C->C->bool.
+Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
+Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
+Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).
+
+Instance equalityb_coef : Equalityb C :=
+  {equalityb x y := Ceqb x y}.
+
+ Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
+  match P, P' with
+  | Pc c, Pc c' => c =? c'
+  | PX P i n Q, PX P' i' n' Q' =>
+    match Pcompare i i' Eq, Pcompare n n' Eq with
+    | Eq, Eq => if Peq P P' then Peq Q Q' else false
+    | _,_ => false
+    end
+  | _, _ => false
+  end.
+
+Instance equalityb_pol : Equalityb Pol :=
+  {equalityb x y := Peq x y}.
+
+(* Q a ses variables de queue < i *)
+ Definition mkPX P i n Q :=
+  match P with
+  | Pc c => if c =? 0 then Q else PX P i n Q 
+  | PX P' i' n' Q' => 
+       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
+  end.
+
+ Definition mkXi i n := PX P1 i n P0.
+
+ Definition mkX i := mkXi i 1.
+
+ (** Opposite of addition *)
+
+ Fixpoint Popp (P:Pol) : Pol :=
+  match P with
+  | Pc c => Pc (- c)
+  | PX P i n Q => PX (Popp P) i n (Popp Q)
+  end.
+
+ Notation "-- P" := (Popp P)(at level 30).
+
+ (** Addition et subtraction *)
+
+ Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol :=
+  match P with
+  | Pc c1 => Pc (c + c1)
+  | PX P i n Q => PX P i n (PaddCl c Q)
+  end.
+
+(* Q quelconque *)
+
+Section PaddX.
+Variable Padd:Pol->Pol->Pol.
+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 *)
+
+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 Pcompare i i' Eq with
+      | (* i > i' *)
+        Gt => mkPX P i n Q
+      | (* i < i' *)
+        Lt => mkPX P' i' n' (PaddX i n Q')
+      | (* i = i' *)
+        Eq => match ZPminus n n' with
+              | (* n > n' *) 
+                Zpos k => mkPX (PaddX i k P') i' n' Q'
+              | (* n = n' *)
+                Z0 => mkPX (Padd P P') i n Q'
+              | (* n < n' *)
+                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
+              end
+      end
+  end.
+
+End PaddX.
+
+Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol :=
+  match P1 with
+  | Pc c => PaddCl c P2
+  | PX P' i' n' Q' =>
+      PaddX Padd P' i' n' (Padd Q' P2)
+  end.
+
+ Notation "P ++ P'" := (Padd P P').
+
+Definition Psub(P P':Pol):= P ++ (--P').
+
+ Notation "P -- P'" := (Psub P P')(at level 50).
+
+ (** Multiplication *)
+
+ Fixpoint PmulC_aux (P:Pol) (c:C)  {struct P} : Pol :=
+  match P with
+  | Pc c' => Pc (c' * c)
+  | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c)
+  end.
+
+ Definition PmulC 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
+   | Pc c => PmulC P1 c
+   | PX P i n Q =>
+     PaddX Padd (Pmul P1 P) i n (Pmul P1 Q)
+   end.
+
+ Notation "P ** P'" := (Pmul P P')(at level 40).
+
+ Definition Psquare (P:Pol) : Pol := P ** P.
+
+
+ (** Evaluation of a polynomial towards R *)
+
+ Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
+  match P with
+  | Pc c => [c]
+  | PX P i n Q =>
+     let x := nth 0 i l in
+     let xn := pow_pos x n in
+   (Pphi l P) * xn + (Pphi l Q)
+  end.
+
+ Reserved Notation "P @ l " (at level 10, no associativity).
+ Notation "P @ l " := (Pphi l P).
+ (** Proofs *)
+ Lemma ZPminus_spec : forall x y,
+  match ZPminus x y with
+  | Z0 => x = y
+  | Zpos k => x = (y + k)%positive
+  | Zneg k => y = (x + k)%positive
+  end.
+ Proof.
+  induction x;destruct y.
+  replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));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 (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 (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.
+  replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
+  replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
+  rewrite <- Pplus_one_succ_l.
+  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
+  simpl;trivial.
+ Qed.
+
+ 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.
+  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. 
+ rewrite ring_morphism0. reflexivity.
+ Qed.
+
+ Lemma Pphi1 : forall l,  P1@l == 1.
+ Proof.
+  intros;simpl; rewrite ring_morphism1. reflexivity.
+ Qed.
+
+ Lemma mkPX_ok : forall l P i n Q,
+  (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;reflexivity).
+  assert (Hh := ring_morphism_eq  c 0). 
+simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
+intros.
+  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 :=
+  repeat (progress (
+   match goal with
+   | |- context [?P@?l] =>
+       match P with
+       | 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
+       | 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));
+  simpl; rsimpl.
+
+ Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
+ Proof.
+  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;simpl;intros.  rewrite ring_morphism_mul.
+try reflexivity.
+  simpl. Esimpl.  rewrite IHP1;rewrite IHP2;rsimpl. 
+  Qed.
+
+ Lemma PmulC_ok : forall c P l, (PmulC P c)@l ==  P@l * [c].
+ Proof.
+  intros c P l; unfold PmulC.
+  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;simpl;intros.
+  Esimpl.
+  rewrite IHP1;rewrite IHP2;rsimpl.
+ Qed.
+
+ Ltac Esimpl2 :=
+  Esimpl;
+  repeat (progress (
+   match goal with
+   | |- 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,
+  PaddX Padd P i n Q =
+  match Q with
+  | Pc c => mkPX P i n Q
+  | PX P' i' n' Q' => 
+      match Pcompare i i' Eq with
+      | (* i > i' *)
+        Gt => mkPX P i n Q
+      | (* i < i' *)
+        Lt => mkPX P' i' n' (PaddX Padd P i n Q')
+      | (* i = i' *)
+        Eq => match ZPminus n n' with
+              | (* n > n' *) 
+                Zpos k => mkPX (PaddX Padd P i k P') i' n' Q'
+              | (* n = n' *)
+                Z0 => mkPX (Padd P P') i n Q'
+              | (* n < n' *)
+                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
+              end
+      end
+  end.
+induction Q; reflexivity.
+Qed.
+
+Lemma PaddX_ok2 : forall P2,
+   (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l)
+   /\
+   (forall P k n l,
+           (PaddX Padd P2 k n P) @ l == 
+             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. rewrite H0. rewrite H1.
+Esimpl2.
+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.
+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 (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. rewrite Padd_ok. rewrite Popp_ok. rsimpl.
+ Qed.
+
+ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+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.
+ Proof.
+  intros. unfold Psquare. apply Pmul_ok.
+ Qed.
+
+ (** Definition of polynomial expressions *)
+
+(*
+ Inductive PExpr : Type :=
+  | PEc : C -> PExpr
+  | PEX : positive -> PExpr
+  | PEadd : PExpr -> PExpr -> PExpr
+  | PEsub : PExpr -> PExpr -> PExpr
+  | PEmul : PExpr -> PExpr -> PExpr
+  | PEopp : PExpr -> PExpr
+  | PEpow : PExpr -> N -> PExpr.
+*)
+
+ (** Specification of the power function *)
+ Section POWER.
+  Variable Cpow : Set.
+  Variable Cp_phi : N -> Cpow.
+  Variable rpow : R -> Cpow -> R.
+
+  Record power_theory : Prop := mkpow_th {
+    rpow_pow_N : forall r n,  (rpow r (Cp_phi n))== (pow_N r n)
+  }.
+
+ End POWER.
+ Variable Cpow : Set.
+ Variable Cp_phi : N -> Cpow.
+ Variable rpow : R -> Cpow -> R.
+ Variable pow_th : power_theory Cp_phi rpow.
+
+ (** evaluation of polynomial expressions towards R *)
+ Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
+   match pe with
+   | PEc c => [c]
+   | PEX j => nth 0 j l
+   | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
+   | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
+   | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
+   | PEopp pe1 => - (PEeval l pe1)
+   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
+   end.
+
+Strategy expand [PEeval].
+
+ Definition mk_X j := mkX j.
+
+ (** Correctness proofs *)
+
+ Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
+ Proof.
+  destruct p;simpl;intros;Esimpl;trivial.
+ Qed.
+
+ Ltac Esimpl3 :=
+  repeat match goal with
+  | |- 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 *)
+
+Section POWER2.
+  Variable subst_l : Pol -> Pol.
+  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
+   match p with
+   | xH => subst_l (Pmul P res)
+   | xO p => Ppow_pos (Ppow_pos res P p) P p
+   | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p))
+   end.
+
+  Definition Ppow_N P n :=
+   match n with
+   | N0 => P1
+   | Npos p => Ppow_pos P1 P p
+   end.
+
+  Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R :=
+  match i with
+  | xH => x
+  | xO i => let p := pow_pos_gen m x i in m p p
+  | xI i => let p := pow_pos_gen m x i in m x (m p p)
+  end.
+
+Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
+         forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l.
+  Proof.
+   intros l subst_l_ok res P p. generalize res;clear res.
+   induction p;simpl;intros. try rewrite subst_l_ok.
+ repeat rewrite Pmul_ok. repeat rewrite IHp.
+   rsimpl. 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) :=
+  match p with
+  | N0 => x1
+  | Npos p => pow_pos_gen m x p
+  end.
+
+  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;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl.  Qed.
+
+ End POWER2.
+
+ (** Normalization and rewriting *)
+
+ Section NORM_SUBST_REC.
+  Let subst_l (P:Pol) := P.
+  Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
+  Let Ppow_subst := Ppow_N subst_l.
+
+  Fixpoint norm_aux (pe:PExpr C) : Pol :=
+   match pe with
+   | PEc c => Pc c
+   | PEX j => mk_X j
+   | PEadd pe1 (PEopp pe2) =>
+     Psub (norm_aux pe1) (norm_aux pe2)
+   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
+   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
+   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
+   | PEopp pe1 => Popp (norm_aux pe1)
+   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
+   end.
+
+  Definition norm_subst pe := subst_l (norm_aux pe).
+
+ 
+ Lemma norm_aux_spec :
+     forall l pe, 
+       PEeval l pe == (norm_aux pe)@l.
+  Proof.
+   intros.
+   induction pe.
+Esimpl3. Esimpl3. simpl.
+ rewrite IHpe1;rewrite IHpe2.
+ destruct pe2; Esimpl3. 
+unfold Psub.
+destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
+simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
+destruct pe1. destruct pe2; rewrite Padd_ok; rewrite Popp_ok; try reflexivity.
+Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+ Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
+simpl. rewrite IHpe; Esimpl3. 
+simpl.
+   rewrite Ppow_N_ok; (intros;try reflexivity). 
+   rewrite rpow_pow_N.  Esimpl3.
+   induction n;simpl. Esimpl3. induction p; simpl.
+  try rewrite IHp;try rewrite IHpe;
+ repeat rewrite Pms_ok;
+      repeat rewrite Pmul_ok;reflexivity.
+rewrite Pmul_ok. try rewrite IHp;try rewrite IHpe;
+ repeat rewrite Pms_ok;
+      repeat rewrite Pmul_ok;reflexivity. trivial.
+exact pow_th.
+  Qed.
+
+ Lemma norm_subst_spec :
+     forall l pe, 
+       PEeval l pe == (norm_subst pe)@l.
+ Proof.
+  intros;unfold norm_subst.
+  unfold subst_l.  apply norm_aux_spec. 
+ Qed.
+
+ End NORM_SUBST_REC.
+
+ Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop :=
+   match lpe with
+   | nil => True
+   | (me,pe)::lpe =>
+     match lpe with
+     | nil => PEeval l me == PEeval l pe
+     | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe
+     end
+  end.
+
+
+ Lemma norm_subst_ok : forall l pe,
+   PEeval l pe == (norm_subst pe)@l.
+ Proof.
+   intros;apply norm_subst_spec. 
+  Qed.
+
+
+ Lemma ring_correct : forall l pe1 pe2,
+   (norm_subst pe1 =? norm_subst pe2) = true ->
+   PEeval l pe1 == PEeval l pe2.
+ Proof.
+  simpl;intros.
+  do 2 (rewrite (norm_subst_ok l);trivial).
+  apply Peq_ok;trivial.
+ Qed.
+
+End MakeRingPol.
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
new file mode 100644
index 00000000..34731eb3
--- /dev/null
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -0,0 +1,308 @@
+(************************************************************************)
+(*  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.
+Require Import Algebra_syntax.
+Require Export Ncring.
+Require Import Ncring_polynom.
+Require Import Ncring_initial.
+
+
+Set Implicit Arguments.
+
+Class nth (R:Type) (t:R) (l:list R) (i:nat).
+
+Instance  Ifind0 (R:Type) (t:R) l
+ : nth t(t::l) 0.
+
+Instance  IfindS (R:Type) (t2 t1:R) l i 
+ {_: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  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)}
+ {_: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)|10.
+
+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 
+ `{nth R t lvar i}
+ `{Rr: Ring (T:=R)}
+ : reify (Rr:= Rr) (PEX Z (P_of_succ_nat i))lvar t 
+ | 100.
+
+Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) 
+  (lterm:list R).
+
+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 
+ `{Rr: Ring (T:=R)}
+ {_:reifylist (Rr:= Rr) lexpr lvar lterm}
+ `{closed (T:=R) lvar}  := (lvar,lexpr).
+
+Unset Implicit Arguments.
+
+
+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.
+ intros x y H. rewrite (Zeq_bool_eq x y H). reflexivity. Qed. 
+
+Ltac reify_goal lvar lexpr lterm:=
+  (*idtac lvar; idtac lexpr; idtac lterm;*)
+  match lexpr with
+     nil => idtac
+   | ?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. 
+
+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_rewrite. intro IHp.  rewrite IHp. reflexivity.
+simpl. generalize IHp. clear IHp.
+gen_rewrite. intro IHp.  rewrite IHp. reflexivity.
+simpl.  gen_rewrite. Qed.
+
+Ltac ring_gen :=
+   match goal with
+     |- ?g => let lterm := lterm_goal g in 
+       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 => 
+               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.
+
+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/Ring.v b/plugins/setoid_ring/Ring.v
index 7b48f590..c44c2edf 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index 9bc95a7f..6d4360d6 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index d33a095f..b722a31b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -38,7 +38,7 @@ Section MakeRingPol.
                                 cO cI cadd cmul csub copp ceqb phi.
 
   (* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.
  Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -104,12 +104,12 @@ Section MakeRingPol.
   match P, P' with
   | Pc c, Pc c' => c ?=! c'
   | Pinj j Q, Pinj j' Q' =>
-    match Pcompare j j' Eq with
+    match j ?= j' with
     | Eq => Peq Q Q'
     | _ => false
     end
   | PX P i Q, PX P' i' Q' =>
-    match Pcompare i i' Eq with
+    match i ?= i' with
     | Eq => if Peq P P' then Peq Q Q' else false
     | _ => false
     end
@@ -435,7 +435,7 @@ Section MakeRingPol.
             CFactor P c
    | Pc _, _    => (P, Pc cO)
    | Pinj j1 P1, zmon j2 M1 =>
-      match (j1 ?= j2) Eq with
+      match j1 ?= j2 with
         Eq => let (R,S) := MFactor P1 c M1 in
                  (mkPinj j1 R, mkPinj j1 S)
       | Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in
@@ -449,7 +449,7 @@ Section MakeRingPol.
              let (R2, S2) := MFactor Q1 c M2 in
                (mkPX R1 i R2, mkPX S1 i S2)
   | PX P1 i Q1, vmon j M1 =>
-      match (i ?= j) Eq with
+      match i ?= j with
         Eq => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in
                  (mkPX R1 i Q1, S1)
       | Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in
@@ -552,10 +552,10 @@ Section MakeRingPol.
  Proof.
   induction P;destruct P';simpl;intros;try discriminate;trivial.
   apply (morph_eq CRmorph);trivial.
-  assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
+  assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
    try discriminate H.
   rewrite (IHP P' H); rewrite H1;trivial;rrefl.
-  assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
+  assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
    try discriminate H.
   rewrite H1;trivial. clear H1.
   assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2);
@@ -947,8 +947,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    generalize (Mcphi_ok P c (jump i l)); case CFactor.
    intros R1 Q1 HH; rewrite HH; Esimpl.
      intros j M.
-     case_eq ((i ?= j) Eq); intros He; simpl.
-       rewrite (Pcompare_Eq_eq _ _ He).
+     case_eq (i ?= j); intros He; simpl.
+       rewrite (Pos.compare_eq _ _ He).
        generalize (Hrec (c, M) (jump j l)); case (MFactor P c M);
         simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
        generalize (Hrec (c, (zmon (j -i) M)) (jump i l));
@@ -987,8 +987,8 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
      rewrite (ARadd_comm ARth); rsimpl.
      rewrite zmon_pred_ok;rsimpl.
    intros j M1.
-     case_eq ((i ?= j) Eq); intros He; simpl.
-       rewrite (Pcompare_Eq_eq _ _ He).
+     case_eq (i ?= j); intros He; simpl.
+       rewrite (Pos.compare_eq _ _ He).
        generalize (Hrec1 (c, mkZmon xH M1) l); case (MFactor P2 c (mkZmon xH M1));
         simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
        rewrite H; rewrite mkPX_ok; rsimpl.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 4fbdcbaa..ab992552 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -229,7 +229,7 @@ Section DEFINITIONS.
 
  (** Specification of the power function *)
  Section POWER.
-  Variable Cpow : Set.
+  Variable Cpow : Type.
   Variable Cp_phi : N -> Cpow.
   Variable rpow : R -> Cpow -> R.
 
@@ -590,6 +590,21 @@ Ltac gen_srewrite Rsth Reqe ARth :=
      | progress rewrite <- (ARopp_mul_l ARth)
      | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ].
 
+Ltac gen_srewrite_sr Rsth Reqe ARth :=
+  repeat first
+     [ gen_reflexivity Rsth
+     | progress rewrite (ARopp_zero Rsth Reqe ARth)
+     | rewrite (ARadd_0_l ARth)
+     | rewrite (ARadd_0_r Rsth ARth)
+     | rewrite (ARmul_1_l ARth)
+     | rewrite (ARmul_1_r Rsth ARth)
+     | rewrite (ARmul_0_l ARth)
+     | rewrite (ARmul_0_r Rsth ARth)
+     | rewrite (ARdistr_l ARth)
+     | rewrite (ARdistr_r Rsth Reqe ARth)
+     | rewrite (ARadd_assoc ARth)
+     | rewrite (ARmul_assoc ARth) ].
+
 Ltac gen_add_push add Rsth Reqe ARth x :=
   repeat (match goal with
   | |- context [add (add ?y x) ?z] =>
diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v
new file mode 100644
index 00000000..fd765471
--- /dev/null
+++ b/plugins/setoid_ring/Rings_Q.v
@@ -0,0 +1,30 @@
+Require Export Cring.
+Require Export Integral_domain.
+
+(* 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.
+
+Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
+unfold Qeq. simpl. auto with *. Qed.
+
+Instance Qdi : (Integral_domain (Rcr:=Qcri)). 
+constructor. 
+exact Qmult_integral. exact Q_one_zero. Defined.
diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v
new file mode 100644
index 00000000..fd219c23
--- /dev/null
+++ b/plugins/setoid_ring/Rings_R.v
@@ -0,0 +1,34 @@
+Require Export Cring.
+Require Export Integral_domain.
+
+(* 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.
+
+Lemma R_one_zero: 1%R <> 0%R.
+discrR.
+Qed.
+
+Instance Rdi : (Integral_domain (Rcr:=Rcri)). 
+constructor. 
+exact Rmult_integral. exact R_one_zero. Defined.
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
new file mode 100644
index 00000000..88904865
--- /dev/null
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -0,0 +1,14 @@
+Require Export Cring.
+Require Export Integral_domain.
+Require Export Ncring_initial.
+
+Instance Zcri: (Cring (Rr:=Zr)).
+red. exact Zmult_comm. Defined.
+
+Lemma Z_one_zero: 1%Z <> 0%Z.
+omega. 
+Qed.
+
+Instance Zdi : (Integral_domain (Rcr:=Zcri)). 
+constructor. 
+exact Zmult_integral. exact Z_one_zero. Defined.
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 362542b9..d3ed36ee 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -27,11 +27,7 @@ Ltac isZpow_coef t :=
   | _ => constr:false
   end.
 
-Definition N_of_Z x :=
- match x with
- | Zpos p => Npos p
- | _ => N0
- end.
+Notation N_of_Z := Z.to_N (only parsing).
 
 Ltac Zpow_tac t :=
  match isZpow_coef t with
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 820246af..9d61c06d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pp
 open Util
 open Names
@@ -18,8 +16,7 @@ open Closure
 open Environ
 open Libnames
 open Tactics
-open Rawterm
-open Termops
+open Glob_term
 open Tacticals
 open Tacexpr
 open Pcoq
@@ -87,7 +84,7 @@ let interp_map l c =
   with Not_found -> None
 
 let interp_map l t =
-  try Some(List.assoc t l) with Not_found -> None
+  try Some(list_assoc_f eq_constr t l) with Not_found -> None
 
 let protect_maps = ref Stringmap.empty
 let add_map s m = protect_maps := Stringmap.add s m !protect_maps
@@ -98,13 +95,13 @@ let lookup_map map =
 
 let protect_red map env sigma c =
   kl (create_clos_infos betadeltaiota env)
-    (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);;
+    (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
 
 let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));;
+  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));;
 
 
 TACTIC EXTEND protect_fv
@@ -144,7 +141,7 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in
   TacFun([Some(id_of_string"t")],
   TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
-  [Genarg.in_gen Genarg.globwit_constr (RVar(dummy_loc,id_of_string"t"),None);
+  [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None);
    Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
 (*
 let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
@@ -161,18 +158,18 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c
 let decl_constant na c =
   mkConst(declare_constant (id_of_string na) (DefinitionEntry
     { const_entry_body = c;
+      const_entry_secctx = None;
       const_entry_type = None;
-      const_entry_opaque = true;
-      const_entry_boxed = true},
+      const_entry_opaque = true },
     IsProof Lemma))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+  TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
 
 let ltac_letin (x, e1) e2 =
   TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
@@ -188,8 +185,10 @@ let ltac_record flds =
 let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
 
 let dummy_goal env =
-  {Evd.it = Evd.make_evar (named_context_val env) mkProp;
-   Evd.sigma = Evd.empty}
+  let (gl,_,sigma) = 
+    Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
+  {Evd.it = gl;
+   Evd.sigma = sigma}
 
 let exec_tactic env n f args =
   let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
@@ -344,7 +343,7 @@ type ring_info =
       ring_pre_tac : glob_tactic_expr;
       ring_post_tac : glob_tactic_expr }
 
-module Cmap = Map.Make(struct type t = constr let compare = compare end)
+module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
 
 let from_carrier = ref Cmap.empty
 let from_relation = ref Cmap.empty
@@ -415,7 +414,7 @@ let subst_th (subst,th) =
   let posttac'= subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
-     set' = th.ring_setoid &&
+     eq_constr set' th.ring_setoid &&
      ext' == th.ring_ext &&
      morph' == th.ring_morph &&
      th' == th.ring_th &&
@@ -440,7 +439,7 @@ let subst_th (subst,th) =
       ring_post_tac = posttac' }
 
 
-let (theory_to_obj, obj_to_theory) =
+let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
@@ -576,13 +575,13 @@ let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
   match kind_of_term th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when f = Lazy.force coq_almost_ring_theory ->
+        when eq_constr f (Lazy.force coq_almost_ring_theory) ->
           (None,r,zero,one,add,mul,Some sub,Some opp,req)
     | App(f,[|r;zero;one;add;mul;req|])
-        when f = Lazy.force coq_semi_ring_theory ->
+        when eq_constr f (Lazy.force coq_semi_ring_theory) ->
         (Some true,r,zero,one,add,mul,None,None,req)
     | App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when f = Lazy.force coq_ring_theory ->
+        when eq_constr f (Lazy.force coq_ring_theory) ->
         (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"
 
@@ -592,10 +591,10 @@ let dest_morph env sigma m_spec =
   match kind_of_term m_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req;
               c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when f = Lazy.force coq_ring_morph ->
+        when eq_constr f (Lazy.force coq_ring_morph) ->
           (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
     | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when f = Lazy.force coq_semi_morph ->
+        when eq_constr f (Lazy.force coq_semi_morph) ->
         (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
     | _ -> error "bad morphism structure"
 
@@ -626,23 +625,23 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
         (match rk, opp, kind with
             Abstract, None, _ ->
               let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
-              TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
+              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
           | Abstract, Some opp, Some _ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
-              TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | Abstract, Some opp, None ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
               TacArg
-                (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | Computational _,_,_ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
               TacArg
-                (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
           | Morphism mth,_,_ ->
               let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
               TacArg
-                (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
+                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
 
 let make_hyp env c =
   let t = Retyping.get_type_of env Evd.empty c in
@@ -659,7 +658,7 @@ let interp_power env pow =
   match pow with
   | None ->
       let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+      (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
@@ -832,7 +831,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t]
+    [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t]
 END
 
 
@@ -893,18 +892,18 @@ let dest_field env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
   match kind_of_term th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when f = Lazy.force afield_theory ->
+        when eq_constr f (Lazy.force afield_theory) ->
         let rth = lapp af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when f = Lazy.force field_theory ->
+        when eq_constr f (Lazy.force field_theory) ->
         let rth =
           lapp f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when f = Lazy.force sfield_theory ->
+        when eq_constr f (Lazy.force sfield_theory) ->
         let rth = lapp sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
@@ -1016,7 +1015,7 @@ let subst_th (subst,th) =
       field_pre_tac = pretac';
       field_post_tac = posttac' }
 
-let (ftheory_to_obj, obj_to_ftheory) =
+let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
@@ -1160,5 +1159,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ]
+      [ let (t,l) = list_sep_last lt in field_lookup f lH l t ]
 END
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 6934375b..580df9b5 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -13,3 +13,13 @@ Ring_tac.vo
 Ring_theory.vo
 Ring.vo
 ZArithRing.vo
+Algebra_syntax.vo
+Cring.vo
+Ncring.vo
+Ncring_polynom.vo
+Ncring_initial.vo
+Ncring_tac.vo
+Rings_Z.vo
+Rings_R.vo
+Rings_Q.vo
+Integral_domain.vo
\ No newline at end of file