mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

28 files changed, 1278 insertions, 1416 deletions

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index fb6a31e99..9298736d0 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -9,7 +9,7 @@
 (* $Id$ *)
 
 Require Import List.
-Require Import Ring.
+Require Import LegacyRing.
 Require Export Field_Compl.
 Require Export Field_Theory.
 
@@ -289,11 +289,12 @@ Ltac field_gen_aux FT :=
               apply_simplif ltac:(apply_inverse mul);
               let id := grep_mult in
               clear id; weak_reduce; clear ft vm; first
-              [ inverse_test FT; ring | field_gen_aux FT ]
+              [ inverse_test FT; legacy ring | field_gen_aux FT ]
            | idtac ] ])
   end.
 
-Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
+Ltac field_gen FT :=
+  unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.
 
 (*****************************)
 (*    Term Simplification    *)
@@ -429,4 +430,4 @@ Ltac field_term FT exp :=
    simpl_all_monomials
     ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
   let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
-  (replace exp with trep; [ ring trep | field_gen FT ]).
+  (replace exp with trep; [ legacy ring trep | field_gen FT ]).
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 5fe69ddca..74d97f163 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -10,7 +10,7 @@
 
 Require Import List.
 Require Import Peano_dec.
-Require Import Ring.
+Require Import LegacyRing.
 Require Import Field_Compl.
 
 Record Field_Theory : Type := 
@@ -88,10 +88,10 @@ Let AinvT := Ainv T.
 Let RTT := RT T.
 Let Th_inv_defT := Th_inv_def T.
 
-Add Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
+Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
  Azero T) (Aopp T) (Aeq T) (RT T).
 
-Add Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
+Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
 
 (***************************)
 (*    Lemmas to be used    *)
@@ -99,55 +99,55 @@ Add Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
 
 Lemma AplusT_sym : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AplusT_assoc :
  forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AmultT_sym : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AmultT_assoc :
  forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma AmultT_AplusT_distr :
  forall r1 r2 r3:AT,
    AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).
 Proof.
-  intros; ring.
+  intros; legacy ring.
 Qed.
 
 Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2.
 Proof.
   intros; transitivity (AplusT (AplusT (AoppT r) r) r1).
-  ring.
+  legacy ring.
   transitivity (AplusT (AplusT (AoppT r) r) r2).
   repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
-  ring.
+  legacy ring.
 Qed.
  
 Lemma r_AmultT_mult :
@@ -162,17 +162,17 @@ Qed.
 
 Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
 Proof.
-  intro; ring.
+  intro; legacy ring.
 Qed.
  
 Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
 Proof.
-  intro; ring.
+  intro; legacy ring.
 Qed.
  
 Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
 Proof.
-  intro; ring.
+  intro; legacy ring.
 Qed.
  
 Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
@@ -183,7 +183,7 @@ Qed.
 Lemma Rmult_neq_0_reg :
  forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.
 Proof.
-  intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; ring.
+  intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring.
 Qed.
 
 (************************)
@@ -276,7 +276,7 @@ Lemma merge_mult_correct :
    interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
 Proof.
 simple induction e1; auto; intros.
-elim e0; try (intros; simpl in |- *; ring).
+elim e0; try (intros; simpl in |- *; legacy ring).
 unfold interp_ExprA in H2; fold interp_ExprA in H2;
  cut
   (AmultT (interp_ExprA lvar e2)
@@ -286,8 +286,8 @@ unfold interp_ExprA in H2; fold interp_ExprA in H2;
      (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4))
         (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
 intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1;
- simpl in |- *; ring.
-ring.
+ simpl in |- *; legacy ring.
+legacy ring.
 Qed.
 
 Lemma assoc_mult_correct1 :
@@ -308,7 +308,7 @@ Lemma assoc_mult_correct :
 Proof.
 simple induction e; auto; intros.
 elim e0; intros.
-intros; simpl in |- *; ring.
+intros; simpl in |- *; legacy ring.
 simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
  rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0.
 simpl in |- *; rewrite (H0 lvar); auto.
@@ -319,7 +319,7 @@ simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
  fold interp_ExprA in H1; rewrite (H0 lvar) in H1;
  rewrite (AmultT_sym (interp_ExprA lvar e3) (interp_ExprA lvar e1));
  rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; 
- ring.
+ legacy ring.
 simpl in |- *; rewrite (H0 lvar); auto.
 simpl in |- *; rewrite (H0 lvar); auto.
 simpl in |- *; rewrite (H0 lvar); auto.
@@ -344,7 +344,7 @@ Lemma merge_plus_correct :
    interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
 Proof.
 simple induction e1; auto; intros.
-elim e0; try intros; try (simpl in |- *; ring).
+elim e0; try intros; try (simpl in |- *; legacy ring).
 unfold interp_ExprA in H2; fold interp_ExprA in H2;
  cut
   (AplusT (interp_ExprA lvar e2)
@@ -354,8 +354,8 @@ unfold interp_ExprA in H2; fold interp_ExprA in H2;
      (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4))
         (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
 intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1;
- simpl in |- *; ring.
-ring.
+ simpl in |- *; legacy ring.
+legacy ring.
 Qed.
 
 Lemma assoc_plus_correct :
@@ -455,7 +455,7 @@ Lemma distrib_mult_right_correct :
 Proof.
 simple induction e1; try intros; simpl in |- *; auto.
 rewrite AmultT_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
- rewrite (H0 e2 lvar); ring.
+ rewrite (H0 e2 lvar); legacy ring.
 Qed.
 
 Lemma distrib_mult_left_correct :
@@ -491,7 +491,7 @@ simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar);
  unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct.
 simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar);
  unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct;
- simpl in |- *; fold AoppT in |- *; ring.
+ simpl in |- *; fold AoppT in |- *; legacy ring.
 Qed.
 
 (**** Multiplication by the inverse product ****)
@@ -527,7 +527,7 @@ Lemma multiply_aux_correct :
 Proof.
 simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
  auto.
-  simpl in |- *; rewrite (H0 lvar); ring.
+  simpl in |- *; rewrite (H0 lvar); legacy ring.
 Qed.
 
 Lemma multiply_correct :
@@ -595,8 +595,8 @@ simpl in |- *; case (eqExprA e0 (EAinv a)); intros.
 rewrite e2; simpl in |- *; fold AinvT in |- *.
 rewrite <-
  (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
-    (interp_ExprA lvar e1)); rewrite AinvT_r; [ ring | assumption ].
-simpl in |- *; rewrite H0; auto; ring.
+    (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ].
+simpl in |- *; rewrite H0; auto; legacy ring.
 simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a));
  intros; [ inversion e1 | simpl in |- *; trivial ].
 unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros.
@@ -619,7 +619,7 @@ simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct;
 elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1);
  intros.
 rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto.
-ring.
+legacy ring.
 Qed.
 
 Lemma monom_simplif_correct :
diff --git a/contrib/field/Field.v b/contrib/field/LegacyField.v
index 5d08c57f4..5d08c57f4 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/LegacyField.v
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 8e33f6292..f8f872134 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -139,7 +139,7 @@ ARGUMENT EXTEND minus_div_arg
 END
 
 VERNAC COMMAND EXTEND Field
-  [ "Add" "Field" 
+  [ "Add" "Legacy" "Field" 
       constr(a) constr(aplus) constr(amult) constr(aone)
       constr(azero) constr(aopp) constr(aeq)
       constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
@@ -153,7 +153,7 @@ END
 
 (* Guesses the type and calls field_gen with the right theory *)
 let field g =
-  Coqlib.check_required_library ["Coq";"field";"Field"];
+  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
   let typ = 
     match Hipattern.match_with_equation (pf_concl g) with
       | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
@@ -187,7 +187,7 @@ let field_term l g =
 
 (* Declaration of Field *)
 
-TACTIC EXTEND field
-| [ "field" ] -> [ field ]
-| [ "field" ne_constr_list(l) ] -> [ field_term l ]
+TACTIC EXTEND legacy_field
+| [ "legacy" "field" ] -> [ field ]
+| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
 END
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index a97869b32..ac1592bee 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -17,7 +17,7 @@ Declare ML Module "fourierR".
 Declare ML Module "field".
 
 Require Export Fourier_util.
-Require Export Field.
+Require Export LegacyField.
 Require Export DiscrR.
 
 Ltac fourier := abstract (fourierz; field; discrR).
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 97dfbfb1e..b6cc55f61 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -46,7 +46,7 @@ and ct_COMMAND =
   | CT_coerce_THEOREM_GOAL_to_COMMAND of ct_THEOREM_GOAL
   | CT_abort of ct_ID_OPT_OR_ALL
   | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST
-  | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_BINDING_LIST
+  | CT_add_field of ct_FORMULA * ct_FORMULA * ct_FORMULA * ct_FORMULA_OPT
   | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_addpath of ct_STRING * ct_ID_OPT
   | CT_arguments_scope of ct_ID * ct_ID_OPT_LIST
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index e1b8e7125..890bb3ce5 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -336,7 +336,7 @@ let debug_tac = function
 add_tactic "DebugTac" debug_tac;;
 *)
 
-Refiner.add_tactic "OnThen" on_then;;
+Tacinterp.add_tactic "OnThen" on_then;;
 
 let rec clean_path tac l = 
   match tac, l with
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 9c26c0711..fe227f995 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -112,19 +112,12 @@ and fCOMMAND = function
    fFORMULA x2;
    fINT_LIST x3;
    fNODE "abstraction" 3
-| CT_add_field(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) ->
+| CT_add_field(x1, x2, x3, x4) ->
    fFORMULA x1;
    fFORMULA x2;
    fFORMULA x3;
-   fFORMULA x4;
-   fFORMULA x5;
-   fFORMULA x6;
-   fFORMULA x7;
-   fFORMULA x8;
-   fFORMULA x9;
-   fFORMULA x10;
-   fBINDING_LIST x11;
-   fNODE "add_field" 11
+   fFORMULA_OPT x4;
+   fNODE "add_field" 4
 | CT_add_natural_feature(x1, x2) ->
    fNATURAL_FEATURE x1;
    fID x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 292a42873..a7288de9a 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1670,27 +1670,14 @@ let rec xlate_vernac =
 	CT_no_inline(CT_id_ne_list(loc_qualid_to_ct_ID fst,
 				List.map loc_qualid_to_ct_ID l2))
     | VernacExtend("Field", 
-		   [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl;minusdiv]) ->
+		   [fth;ainv;ainvl;div]) ->
 	(match List.map (fun v -> xlate_formula(out_gen rawwit_constr v))
-                   [a;aplus;amult;aone;azero;aopp;aeq;ainv;fth;ainvl]
+                   [fth;ainv;ainvl]
  	 with
-             [a1;aplus1;amult1;aone1;azero1;aopp1;aeq1;ainv1;fth1;ainvl1] ->
-	       let bind =
-		 match out_gen Field.rawwit_minus_div_arg minusdiv with
-		     None, None ->
-		       CT_binding_list[]
-		   | Some m, None ->
-		       CT_binding_list[
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m)]
-		   | None, Some d ->
-		       CT_binding_list[
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)]
-		   | Some m, Some d ->
-		       CT_binding_list[
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "minus"), xlate_formula m);
-			 CT_binding(CT_coerce_ID_to_ID_OR_INT (CT_ident "div"), xlate_formula d)] in
-		 CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1,
-			      ainv1, fth1, ainvl1, bind)
+             [fth1;ainv1;ainvl1] ->
+	       let adiv1 =
+                 xlate_formula_opt (out_gen (wit_opt rawwit_constr) div) in
+	       CT_add_field(fth1, ainv1, ainvl1, adiv1)
 	   |_ -> assert false)
   | VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) ->
       let orient = out_gen Extraargs.rawwit_orient o in
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 0d42dabfd..959d66c74 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -10,7 +10,8 @@
 
 (* Instantiation of the Ring tactic for the naturals of Arith $*)
 
-Require Export Ring.
+Require Import Bool.
+Require Export LegacyRing.
 Require Export Arith.
 Require Import Eqdep_dec.
 
@@ -36,12 +37,12 @@ Hint Resolve nateq_prop: arithring.
 
 Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
   split; intros; auto with arith arithring.
-  apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
-  trivial.
+(*  apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
+  trivial.*)
 Defined.
 
 
-Add Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
+Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
 
 Goal forall n:nat, S n = 1 + n.
 intro; reflexivity.
diff --git a/contrib/ring/Ring.v b/contrib/ring/LegacyRing.v
index d0c2b7da3..667e24d53 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/LegacyRing.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Bool.
 Require Export Ring_theory.
@@ -32,5 +32,5 @@ destruct n; destruct m; destruct p; reflexivity.
 destruct x; destruct y; reflexivity || simpl in |- *; tauto.
 Defined.
 
-Add Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
- [ true false ].
\ No newline at end of file
+Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
+ [ true false ].
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v
index 41e3a7d7b..ee9fb3761 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/NArithRing.v
@@ -10,7 +10,8 @@
 
 (* Instantiation of the Ring tactic for the binary natural numbers *)
 
-Require Export Ring.
+Require Import Bool.
+Require Export LegacyRing.
 Require Export ZArith_base.
 Require Import NArith.
 Require Import Eqdep_dec.
@@ -37,8 +38,9 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
     apply Nmult_1_l.
     apply Nmult_0_l.
     apply Nmult_plus_distr_r.
-    apply Nplus_reg_l.
+(*    apply Nplus_reg_l.*)
     apply Neq_prop.
 Qed.
 
-Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
+Add Legacy Semi Ring
+  N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 5d5046393..574c24421 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -129,7 +129,7 @@ Hint Resolve (SR_mult_zero_left T).
 Hint Resolve (SR_mult_zero_left2 T).
 Hint Resolve (SR_distr_left T).
 Hint Resolve (SR_distr_left2 T).
-Hint Resolve (SR_plus_reg_left T).
+(*Hint Resolve (SR_plus_reg_left T).*)
 Hint Resolve (SR_plus_permute T).
 Hint Resolve (SR_mult_permute T).
 Hint Resolve (SR_distr_right T).
@@ -140,7 +140,7 @@ Hint Resolve (SR_plus_zero_right T).
 Hint Resolve (SR_plus_zero_right2 T).
 Hint Resolve (SR_mult_one_right T).
 Hint Resolve (SR_mult_one_right2 T).
-Hint Resolve (SR_plus_reg_right T).
+(*Hint Resolve (SR_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hint Immediate T.
@@ -439,7 +439,7 @@ Hint Resolve (Th_mult_zero_left T).
 Hint Resolve (Th_mult_zero_left2 T).
 Hint Resolve (Th_distr_left T).
 Hint Resolve (Th_distr_left2 T).
-Hint Resolve (Th_plus_reg_left T).
+(*Hint Resolve (Th_plus_reg_left T).*)
 Hint Resolve (Th_plus_permute T).
 Hint Resolve (Th_mult_permute T).
 Hint Resolve (Th_distr_right T).
@@ -449,7 +449,7 @@ Hint Resolve (Th_plus_zero_right T).
 Hint Resolve (Th_plus_zero_right2 T).
 Hint Resolve (Th_mult_one_right T).
 Hint Resolve (Th_mult_one_right2 T).
-Hint Resolve (Th_plus_reg_right T).
+(*Hint Resolve (Th_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hint Immediate T.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index bd22fa39a..6d0d05778 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -356,7 +356,7 @@ Hint Resolve (SR_mult_zero_left T).
 Hint Resolve (SR_mult_zero_left2 T).
 Hint Resolve (SR_distr_left T).
 Hint Resolve (SR_distr_left2 T).
-Hint Resolve (SR_plus_reg_left T).
+(*Hint Resolve (SR_plus_reg_left T).*)
 Hint Resolve (SR_plus_permute T).
 Hint Resolve (SR_mult_permute T).
 Hint Resolve (SR_distr_right T).
@@ -367,7 +367,7 @@ Hint Resolve (SR_plus_zero_right T).
 Hint Resolve (SR_plus_zero_right2 T).
 Hint Resolve (SR_mult_one_right T).
 Hint Resolve (SR_mult_one_right2 T).
-Hint Resolve (SR_plus_reg_right T).
+(*Hint Resolve (SR_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
 Hint Immediate T.
@@ -785,7 +785,7 @@ Hint Resolve (Th_mult_zero_left T).
 Hint Resolve (Th_mult_zero_left2 T).
 Hint Resolve (Th_distr_left T).
 Hint Resolve (Th_distr_left2 T).
-Hint Resolve (Th_plus_reg_left T).
+(*Hint Resolve (Th_plus_reg_left T).*)
 Hint Resolve (Th_plus_permute T).
 Hint Resolve (Th_mult_permute T).
 Hint Resolve (Th_distr_right T).
@@ -796,7 +796,7 @@ Hint Resolve (Th_plus_zero_right T).
 Hint Resolve (Th_plus_zero_right2 T).
 Hint Resolve (Th_mult_one_right T).
 Hint Resolve (Th_mult_one_right2 T).
-Hint Resolve (Th_plus_reg_right T).
+(*Hint Resolve (Th_plus_reg_right T).*)
 Hint Resolve refl_equal sym_equal trans_equal.
 (*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 Hint Immediate T.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 31cc274b2..192ff1f57 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -39,7 +39,7 @@ Record Semi_Ring_Theory : Prop :=
    SR_mult_one_left : forall n:A, 1 * n = n;
    SR_mult_zero_left : forall n:A, 0 * n = 0;
    SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
-   SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;
+(*   SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*)
    SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
 
 Variable T : Semi_Ring_Theory.
@@ -52,10 +52,10 @@ Let plus_zero_left := SR_plus_zero_left T.
 Let mult_one_left := SR_mult_one_left T. 
 Let mult_zero_left := SR_mult_zero_left T.
 Let distr_left := SR_distr_left T.
-Let plus_reg_left := SR_plus_reg_left T.
+(*Let plus_reg_left := SR_plus_reg_left T.*)
 
 Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
-  mult_one_left mult_zero_left distr_left plus_reg_left.
+  mult_one_left mult_zero_left distr_left (*plus_reg_left*).
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *) 
@@ -126,11 +126,11 @@ Qed.
 Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
 intro; elim mult_comm; auto.
 Qed.
-
+(*
 Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
 intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto.
 Qed.
-
+*)
 End Theory_of_semi_rings.
 
 Section Theory_of_rings.
@@ -320,7 +320,7 @@ symmetry  in |- *; apply Th_mult_opp_opp. Qed.
 Lemma Th_opp_zero : - 0 = 0.
 rewrite <- (plus_zero_left (- 0)).
 auto. Qed.
-
+(*
 Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p.
 intros; generalize (f_equal (fun z => - n + z) H).
 repeat rewrite plus_assoc.
@@ -336,7 +336,7 @@ rewrite (plus_comm n m).
 rewrite (plus_comm n p).
 auto.
 Qed.
-
+*)
 Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
 intros.
 repeat rewrite (mult_comm n).
@@ -349,7 +349,7 @@ Qed.
 
 End Theory_of_rings.
 
-Hint Resolve Th_mult_zero_left Th_plus_reg_left: core.
+Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core.
 
 Unset Implicit Arguments.
 
@@ -373,4 +373,4 @@ End product_ring.
 
 Section power_ring.
 
-End power_ring.
\ No newline at end of file
+End power_ring.
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index 9324fb602..075431827 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -32,5 +32,5 @@ Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
 Qed.
 
 (* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
+Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
  [ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index 0cb86dfdd..5ca1bfced 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -12,9 +12,10 @@
 
 open Quote
 open Ring
+open Tacticals
 
 TACTIC EXTEND ring
-  [ "ring" constr_list(l) ] -> [ polynom l ]
+| [ "legacy" "ring" constr_list(l) ] -> [ polynom l ]
 END
 
 (* The vernac commands "Add Ring" and co *)
@@ -23,7 +24,7 @@ let cset_of_constrarg_list l =
   List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
 
 VERNAC COMMAND EXTEND AddRing
-  [ "Add" "Ring" 
+  [ "Add" "Legacy" "Ring" 
           constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
           constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
   -> [ add_theory true false false
@@ -40,7 +41,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 (cset_of_constrarg_list l) ]
 
-| [ "Add" "Semi" "Ring" 
+| [ "Add" "Legacy" "Semi" "Ring" 
       	  constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
           constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
   -> [ add_theory false false false
@@ -57,7 +58,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 (cset_of_constrarg_list l) ]
 
-| [ "Add" "Abstract" "Ring" 
+| [ "Add" "Legacy" "Abstract" "Ring" 
     	  constr(a) constr(aplus) constr(amult) constr(aone)
           constr(azero) constr(aopp) constr(aeq) constr(t) ] 
   -> [ add_theory true true false
@@ -74,7 +75,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 ConstrSet.empty ]
 
-| [ "Add" "Abstract" "Semi" "Ring" 
+| [ "Add" "Legacy" "Abstract" "Semi" "Ring" 
           constr(a) constr(aplus) constr(amult) constr(aone)
           constr(azero) constr(aeq) constr(t) ] 
   -> [ add_theory false true false
@@ -91,7 +92,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 ConstrSet.empty ]
 
-| [ "Add" "Setoid" "Ring"
+| [ "Add" "Legacy" "Setoid" "Ring"
       	  constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) 
 	  constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm)
 	  constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] 
@@ -112,7 +113,7 @@ VERNAC COMMAND EXTEND AddRing
 			 (constr_of t)
 			 (cset_of_constrarg_list l) ]
 
-| [ "Add" "Semi" "Setoid" "Ring" 
+| [ "Add" "Legacy" "Semi" "Setoid" "Ring" 
           constr(a) constr(aequiv) constr(asetth) constr(aplus)
 	  constr(amult) constr(aone) constr(azero) constr(aeq) 
           constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] 
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 3b937c7a6..3c1645d47 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -298,7 +298,7 @@ let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
      | Cast(c,_,_) -> closed_under cset c  
-     | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
+     | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l
      | _ -> false)
     
 (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 48e8763d5..1c5121ef6 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -885,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with
   | _ -> None
 
 let polynom lc gl =
-  Coqlib.check_required_library ["Coq";"ring";"Ring"];
+  Coqlib.check_required_library ["Coq";"ring";"LegacyRing"];
   match lc with 
    (* If no argument is given, try to recognize either an equality or
       a declared relation with arguments c1 ... cn, 
diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v
index 0def087fd..28fc1afba 100644
--- a/contrib/setoid_ring/BinList.v
+++ b/contrib/setoid_ring/BinList.v
@@ -1,46 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Set Implicit Arguments.
 Require Import BinPos.
+Require Import List.
 Open Scope positive_scope.
 
-
 Section LIST.
-
- Variable A:Type.
- Variable default:A.
-
- Inductive list : Type :=
-  | nil : list
-  | cons : A -> list -> list.
-  
- Infix "::" := cons (at level 60, right associativity).
+ Variable A : Type.
+ Variable default : A.
 
  Definition hd l := match l with hd :: _ => hd | _ => default end. 
 
- Definition tl l := match l with _ :: tl => tl | _ => nil end. 
-
- Fixpoint jump (p:positive) (l:list) {struct p} : list :=
+ Fixpoint jump (p:positive) (l:list A) {struct p} : list A :=
   match p with
-  | xH => tl l
+  | xH => tail l
   | xO p => jump p (jump p l)
-  | xI p  => jump p (jump p (tl l))
+  | xI p  => jump p (jump p (tail l))
   end.
 
- Fixpoint nth (p:positive) (l:list) {struct p} : A:=
+ Fixpoint nth (p:positive) (l:list A) {struct p} : A:=
   match p with
   | xH => hd l
   | xO p => nth p (jump p l)
-  | xI p => nth p (jump p (tl l))
+  | xI p => nth p (jump p (tail l))
   end. 
 
- Fixpoint rev_append (rev l : list) {struct l} : list :=
+ Fixpoint rev_append (rev l : list A) {struct l} : list A :=
   match l with
   | nil => rev
   | (cons h t) => rev_append (cons h rev) t 
   end.
  
- Definition rev l : list := rev_append nil l.
+ Definition rev l : list A := rev_append nil l.
 
- Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l).
+ Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
  Proof. 
   induction j;simpl;intros.
   repeat rewrite IHj;trivial.
@@ -71,7 +70,7 @@ Section LIST.
  Qed.
 
  Lemma jump_Pdouble_minus_one : forall i l,
-  (jump (Pdouble_minus_one i) (tl l)) = (jump i (jump i l)).
+  (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)).
  Proof.
   induction i;intros;simpl.
   repeat rewrite jump_tl;trivial.
@@ -80,7 +79,7 @@ Section LIST.
  Qed.
 
  
- Lemma nth_jump : forall p l, nth p (tl l) = hd (jump p l).
+ Lemma nth_jump : forall p l, nth p (tail l) = hd (jump p l).
  Proof.
   induction p;simpl;intros.
   rewrite <-jump_tl;rewrite IHp;trivial.
@@ -89,7 +88,7 @@ Section LIST.
  Qed.
 
  Lemma nth_Pdouble_minus_one :
-  forall p l, nth (Pdouble_minus_one p) (tl l) = nth p (jump p l).
+  forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
  Proof.
   induction p;simpl;intros.
   repeat rewrite jump_tl;trivial.
@@ -99,3 +98,64 @@ Section LIST.
  Qed.
 
 End LIST.
+Notation list := List.list.
+Notation tail := List.tail.
+Notation cons := List.cons.
+Notation nil := List.nil.
+
+Ltac list_fold_right fcons fnil l :=
+  match l with
+  | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl)
+  | nil => fnil
+  end.
+
+Ltac list_fold_left fcons fnil l :=
+  match l with
+  | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
+  | nil => fnil
+  end.
+
+Ltac list_iter f l :=
+  match l with
+  | (cons ?x ?tl) => f x; list_iter f tl
+  | nil => idtac
+  end.
+
+Ltac list_iter_gen seq f l :=
+  match l with
+  | (cons ?x ?tl) =>
+      let t1 _ := f x in
+      let t2 _ := list_iter_gen seq f tl in
+      seq t1 t2
+  | nil => idtac
+  end.
+
+Ltac AddFvTail a l :=
+ match l with
+ | nil          => constr:(cons a l)
+ | (cons a _)   => l
+ | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l')
+ end.
+
+Ltac Find_at a l :=
+ let rec find n l :=
+   match l with
+   | nil => fail 100 "anomaly: Find_at"
+   | (cons a _) => eval compute in n
+   | (cons _ ?l) => find (Psucc n) l
+   end
+ in find 1%positive l.
+
+Ltac check_is_list t :=
+  match t with
+  | cons _ ?l => check_is_list l
+  | nil => idtac
+  | _ => fail 100 "anomaly: failed to build a canonical list"
+  end.
+
+Ltac check_fv l :=
+  check_is_list l;
+  match type of l with 
+  | list _ => idtac
+  | _ => fail 100 "anomaly: built an ill-typed list"
+  end.
diff --git a/contrib/setoid_ring/Pol.v b/contrib/setoid_ring/Pol.v
index 2bf2574fe..ff5608b8a 100644
--- a/contrib/setoid_ring/Pol.v
+++ b/contrib/setoid_ring/Pol.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Set Implicit Arguments.
 Require Import Setoid.
 Require Export BinList.
@@ -5,6 +13,8 @@ Require Import BinPos.
 Require Import BinInt.
 Require Export Ring_th.
 
+Import RingSyntax.
+
 Section MakeRingPol.
  
  (* Ring elements *)     
@@ -329,7 +339,7 @@ Section MakeRingPol.
   | PX P i Q => 
      let x := hd 0 l in
      let xi := pow x i in
-    (Pphi l P) * xi + (Pphi (tl l) Q)      
+    (Pphi l P) * xi + (Pphi (tail l) Q)      
   end.
 
  Reserved Notation "P @ l " (at level 10, no associativity).
@@ -418,7 +428,7 @@ Section MakeRingPol.
  Qed.
 
  Lemma mkPX_ok : forall l P i Q, 
-  (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tl l).
+  (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tail l).
  Proof.
   intros l P i Q;unfold mkPX.
   destruct P;try (simpl;rrefl).
@@ -519,33 +529,33 @@ Section MakeRingPol.
   rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl.
   rewrite IHP'2;simpl.
   rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl.
-  rewrite IHP'2;rsimpl. add_push (P @ (tl l));rrefl.
+  rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl.
   assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
   rewrite IHP'1;rewrite IHP'2;rsimpl.
-  add_push (P3 @ (tl l));rewrite H;rrefl.
+  add_push (P3 @ (tail l));rewrite H;rrefl.
   rewrite IHP'1;rewrite IHP'2;simpl;Esimpl.
   rewrite H;rewrite Pplus_comm.
   rewrite pow_Pplus;rsimpl.
-  add_push (P3 @ (tl l));rrefl.
+  add_push (P3 @ (tail l));rrefl.
   assert (forall P k l, 
            (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k).
    induction P;simpl;intros;try apply (ARadd_sym ARth).
    destruct p2;simpl;try apply (ARadd_sym ARth).
    rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth).
     assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2.
-    rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tl l0));rrefl.
+    rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl.
     rewrite IHP'1;simpl;Esimpl.
     rewrite H1;rewrite Pplus_comm.
     rewrite pow_Pplus;simpl;Esimpl.
-    add_push (P5 @ (tl l0));rrefl.
+    add_push (P5 @ (tail l0));rrefl.
     rewrite IHP1;rewrite H1;rewrite Pplus_comm.
     rewrite pow_Pplus;simpl;rsimpl.
-    add_push (P5 @ (tl l0));rrefl.
+    add_push (P5 @ (tail l0));rrefl.
   rewrite H0;rsimpl.
-  add_push (P3 @ (tl l)).
+  add_push (P3 @ (tail l)).
   rewrite H;rewrite Pplus_comm.
   rewrite IHP'2;rewrite pow_Pplus;rsimpl.
-  add_push (P3 @ (tl l));rrefl.
+  add_push (P3 @ (tail l));rrefl.
  Qed.
 
  Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
@@ -569,17 +579,17 @@ Section MakeRingPol.
   repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl.
   destruct p0;simpl;Esimpl2.
   rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));trivial.
-  add_push (P @ (jump p0 (jump p0 (tl l))));rrefl.
+  add_push (P @ (jump p0 (jump p0 (tail l))));rrefl.
   rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl.
   add_push (- (P'1 @ l * pow (hd 0 l) p));rrefl.
-  rewrite IHP'2;rsimpl;add_push (P @ (tl l));rrefl.
+  rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl.
   assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
   rewrite IHP'1; rewrite IHP'2;rsimpl.
-  add_push (P3 @ (tl l));rewrite H;rrefl.
+  add_push (P3 @ (tail l));rewrite H;rrefl.
    rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl.
   rewrite H;rewrite Pplus_comm.
   rewrite pow_Pplus;rsimpl.
-  add_push (P3 @ (tl l));rrefl.
+  add_push (P3 @ (tail l));rrefl.
   assert (forall P k l, 
            (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k).
    induction P;simpl;intros.
@@ -589,15 +599,15 @@ Section MakeRingPol.
    rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth);trivial.
    apply (ARadd_sym ARth);trivial.
     assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl.
-    rewrite IHP'1;rsimpl;add_push (P5 @ (tl l0));rewrite H1;rrefl.
+    rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl.
     rewrite IHP'1;rewrite H1;rewrite Pplus_comm.
     rewrite pow_Pplus;simpl;Esimpl.
-    add_push (P5 @ (tl l0));rrefl.
+    add_push (P5 @ (tail l0));rrefl.
     rewrite IHP1;rewrite H1;rewrite Pplus_comm.
     rewrite pow_Pplus;simpl;rsimpl.
-    add_push (P5 @ (tl l0));rrefl.
+    add_push (P5 @ (tail l0));rrefl.
   rewrite H0;rsimpl.
-  rewrite IHP'2;rsimpl;add_push (P3 @ (tl l)).
+  rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)).
   rewrite H;rewrite Pplus_comm.
   rewrite pow_Pplus;rsimpl.
  Qed.
@@ -762,7 +772,7 @@ Section MakeRingPol.
   | Pinj j Q => add_mult_dev rP Q (jump j fv) lm
   | PX P i Q => 
      let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in
-     if Q ?== P0 then rP else add_mult_dev rP Q (tl fv) lm
+     if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm
   end.
  
  Definition mkmult1 lm :=
@@ -778,10 +788,10 @@ Section MakeRingPol.
   | Pinj j Q => mult_dev Q (jump j fv) lm
   | PX P i Q => 
      let rP := mult_dev P fv (powl i (hd 0 fv) lm) in
-     if Q ?== P0 then rP else add_mult_dev rP Q (tl fv) lm
+     if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm
   end. 
 
- Definition Pphi_dev fv P := mult_dev P fv (nil R).
+ Definition Pphi_dev fv P := mult_dev P fv nil.
 
  Add Morphism mkmult : mkmult_ext.
   intros r r0 eqr l;generalize l r r0 eqr;clear l r r0 eqr;
@@ -898,15 +908,15 @@ Section MakeRingPol.
   rewrite <- Pphi_mult_dev;simpl;Esimpl.
  Qed.
 
- Lemma Pphi_dev_ok :  forall l pe,  PEeval l pe == Pphi_dev l (norm pe).
+ Lemma Pphi_dev_gen_ok :  forall l pe,  PEeval l pe == Pphi_dev l (norm pe).
  Proof.
   intros l pe;rewrite <- Pphi_Pphi_dev;apply norm_ok.
  Qed.
 
- Lemma Pphi_dev_ok' :
+ Lemma Pphi_dev_ok :
    forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
  Proof.
-  intros l pe npe npe_eq; subst npe; apply Pphi_dev_ok.
+  intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok.
  Qed.
  
 (* The same but building a PExpr *)
@@ -939,7 +949,7 @@ Section MakeRingPol.
   | Pinj j Q => Padd_mult_dev rP Q (jump j fv) lm
   | PX P i Q => 
      let rP := Padd_mult_dev rP P fv (Ppowl i (hd P0 fv) lm) in
-     if Q ?== P0 then rP else Padd_mult_dev rP Q (tl fv) lm
+     if Q ?== P0 then rP else Padd_mult_dev rP Q (tail fv) lm
   end.
  
  Definition Pmkmult1 lm :=
@@ -955,10 +965,10 @@ Section MakeRingPol.
   | Pinj j Q => Pmult_dev Q (jump j fv) lm
   | PX P i Q => 
      let rP := Pmult_dev P fv (Ppowl i (hd (PEc r0) fv) lm) in
-     if Q ?== P0 then rP else Padd_mult_dev rP Q (tl fv) lm
+     if Q ?== P0 then rP else Padd_mult_dev rP Q (tail fv) lm
   end. 
 
- Definition Pphi_dev2 fv P := Pmult_dev P fv (nil PExpr).
+ Definition Pphi_dev2 fv P := Pmult_dev P fv nil.
 
 ...
 *)
@@ -1009,7 +1019,7 @@ Section MakeRingPol.
   | Pinj j Q => Pphi_dev (jump j fv) Q
   | PX P i Q => 
     let rP := mult_dev P fv (pow_dev i (hd 0 fv)) in
-    add_dev rP Q (tl fv)
+    add_dev rP Q (tail fv)
   end
 
  with add_dev (ra:R) (P:Pol) (fv:list R) {struct P} : R :=
@@ -1018,7 +1028,7 @@ Section MakeRingPol.
   | Pinj j Q => add_dev ra Q (jump j fv)
   | PX P i Q =>
     let ra := add_mult_dev ra P fv (pow_dev i (hd 0 fv)) in
-    add_dev ra Q (tl fv)
+    add_dev ra Q (tail fv)
   end
  
  with mult_dev (P:Pol) (fv:list R) (rm:R) {struct P} : R :=
@@ -1027,7 +1037,7 @@ Section MakeRingPol.
   | Pinj j Q => mult_dev Q (jump j fv) rm
   | PX P i Q =>
     let ra := mult_dev P fv (pow_mult i (hd 0 fv) rm) in
-    add_mult_dev ra Q (tl fv) rm
+    add_mult_dev ra Q (tail fv) rm
   end
 
  with add_mult_dev (ra:R) (P:Pol) (fv:list R) (rm:R) {struct P} : R :=
@@ -1037,7 +1047,7 @@ Section MakeRingPol.
   | PX P i Q =>
     let rmP := pow_mult i (hd 0 fv) rm in
     let raP := add_mult_dev ra P fv rmP in
-    add_mult_dev raP Q (tl fv) rm
+    add_mult_dev raP Q (tail fv) rm
   end.
  
  Lemma Pphi_add_mult_dev : forall P ra fv rm,
@@ -1049,7 +1059,7 @@ Section MakeRingPol.
     rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl.
     rrefl.
   apply IHP.
-  rewrite (IHP2 (add_mult_dev ra P2 fv (pow_mult p (hd 0 fv) rm)) (tl fv) rm).
+  rewrite (IHP2 (add_mult_dev ra P2 fv (pow_mult p (hd 0 fv) rm)) (tail fv) rm).
   rewrite (IHP1 ra fv (pow_mult p (hd 0 fv) rm)).
   rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl.
  Qed.
@@ -1062,7 +1072,7 @@ Section MakeRingPol.
     rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl.
     rrefl.
   apply IHP.
-  rewrite (IHP2 (add_mult_dev ra P2 fv (pow_dev p (hd 0 fv))) (tl fv)).
+  rewrite (IHP2 (add_mult_dev ra P2 fv (pow_dev p (hd 0 fv))) (tail fv)).
   rewrite (Pphi_add_mult_dev P2 ra fv (pow_dev p (hd 0 fv))).
   rewrite  (pow_dev_pow p (hd 0 fv));rsimpl. 
  Qed.
@@ -1076,7 +1086,7 @@ Section MakeRingPol.
     rrefl.
   apply IHP.
   rewrite (Pphi_add_mult_dev P3 
-	    (mult_dev P2 fv (pow_mult p (hd 0 fv) rm)) (tl fv) rm).
+	    (mult_dev P2 fv (pow_mult p (hd 0 fv) rm)) (tail fv) rm).
   rewrite (IHP1 fv  (pow_mult p (hd 0 fv) rm)).
   rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl.
  Qed.
@@ -1085,7 +1095,7 @@ Section MakeRingPol.
  Proof.
   induction P;simpl;intros.
   rrefl. trivial.
-  rewrite (Pphi_add_dev P3 (mult_dev P2 fv (pow_dev p (hd 0 fv))) (tl fv)).
+  rewrite (Pphi_add_dev P3 (mult_dev P2 fv (pow_dev p (hd 0 fv))) (tail fv)).
   rewrite (Pphi_mult_dev P2 fv (pow_dev p (hd 0 fv))).
   rewrite (pow_dev_pow p (hd 0 fv));rsimpl.
  Qed.
@@ -1101,7 +1111,7 @@ Section MakeRingPol.
    | (nil _) => constr:(rev)
    | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t 
    end in
- rev_append (nil R) l.
+ rev_append (@nil R) l.
 
  Ltac TPphi_dev add mul :=
   let tl l := match l with (cons ?h ?t) => constr:(t) end in
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
new file mode 100644
index 000000000..45f59a557
--- /dev/null
+++ b/contrib/setoid_ring/Ring.v
@@ -0,0 +1,44 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Bool.
+Require Export Ring_th.
+Require Export Ring_base.
+Require Import ZRing_th.
+Require Import Ring_equiv.
+
+Lemma BoolTheory :
+  ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
+split; simpl in |- *.
+destruct x; reflexivity.
+destruct x; destruct y; reflexivity.
+destruct x; destruct y; destruct z; reflexivity.
+reflexivity.
+destruct x; destruct y; reflexivity.
+destruct x; destruct y; reflexivity.
+destruct x; destruct y; destruct z; reflexivity.
+reflexivity.
+destruct x; reflexivity.
+Qed.
+
+Unboxed Definition bool_eq (b1 b2:bool) :=
+  if b1 then b2 else negb b2.
+
+Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2.
+destruct b1; destruct b2; auto.
+Qed.
+
+Ltac bool_cst t :=
+  let t := eval hnf in t in
+  match t with
+    true => constr:true
+  | false => constr:false
+  | _ => NotConstant
+  end.
+
+Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
new file mode 100644
index 000000000..2209f0643
--- /dev/null
+++ b/contrib/setoid_ring/Ring_base.v
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This module gathers the necessary base to build an instance of the
+   ring tactic. Abstract rings need more theory, depending on
+   ZArith_base. *)
+
+Declare ML Module "newring".
+Require Export Ring_th.
+Require Export Ring_tac.
diff --git a/contrib/setoid_ring/Ring_equiv.v b/contrib/setoid_ring/Ring_equiv.v
new file mode 100644
index 000000000..135a59e01
--- /dev/null
+++ b/contrib/setoid_ring/Ring_equiv.v
@@ -0,0 +1,74 @@
+Require Import Ring_theory.
+Require Import Coq.ring.Setoid_ring_theory.
+Require Import Ring_th.
+
+Set Implicit Arguments.
+
+Section Old2New.
+
+Variable A : Type.
+
+Variable Aplus : A -> A -> A.
+Variable Amult : A -> A -> A.
+Variable Aone : A.
+Variable Azero : A.
+Variable Aopp : A -> A.
+Variable Aeq : A -> A -> bool.
+Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
+
+Let Aminus := fun x y => Aplus x (Aopp y).
+
+Lemma ring_equiv1 :
+  ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
+Proof.
+destruct R.
+split;  eauto.
+Qed.
+
+End Old2New.
+
+Section New2OldRing.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
+
+ Variable reqb : R -> R -> bool.
+ Variable reqb_ok : forall x y, reqb x y = true -> x = y.
+
+ Lemma ring_equiv2 :
+   Ring_Theory radd  rmul rI rO ropp reqb.
+Proof.
+elim Rth; intros; constructor;  eauto.
+intros.
+apply reqb_ok.
+destruct (reqb x y); trivial; intros.
+elim H.
+Qed.
+
+ Definition default_eqb : R -> R -> bool := fun x y => false.
+ Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
+Proof.
+discriminate 1.
+Qed.
+
+End New2OldRing.
+
+Section New2OldSemiRing.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul: R->R->R).
+ Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
+
+ Variable reqb : R -> R -> bool.
+ Variable reqb_ok : forall x y, reqb x y = true -> x = y.
+
+ Lemma sring_equiv2 :
+   Semi_Ring_Theory radd rmul rI rO reqb.
+Proof.
+elim SRth; intros; constructor;  eauto.
+intros.
+apply reqb_ok.
+destruct (reqb x y); trivial; intros.
+elim H.
+Qed.
+
+End New2OldSemiRing.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 6c3f87a5b..a6ac66881 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -1,76 +1,63 @@
 Set Implicit Arguments.
 Require Import Setoid.
-Require Import BinList.
 Require Import BinPos.
 Require Import Pol.
+Require Import BinList.
 Declare ML Module "newring".
 
-(* Some Tactics *)
-
-Ltac compute_assertion id t :=
-  let t' := eval compute in t in
-  (assert (id : t = t'); [exact_no_check (refl_equal t')|idtac]).
-
-Ltac compute_assertion' id  id' t :=
-  let t' := eval compute in t in
+(* adds a definition id' on the normal form of t and an hypothesis id
+   stating that t = id' (tries to produces a proof as small as possible) *)
+Ltac compute_assertion id  id' t :=
+  let t' := eval vm_compute in t in
   (pose (id' := t');
    assert (id : t = id');
    [exact_no_check (refl_equal id')|idtac]).
 
-Ltac compute_replace' id t :=
-  let t' := eval compute in t in
-  (replace t with t' in id; [idtac|exact_no_check (refl_equal t')]).
+(********************************************************************)
+(* Tacticals to build reflexive tactics *)
 
-Ltac bin_list_fold_right fcons fnil l :=
-  match l with
-  | (cons ?x ?tl) => fcons x ltac:(bin_list_fold_right fcons fnil tl)
-  | (nil _) => fnil
-  end.
-
-Ltac bin_list_fold_left fcons fnil l :=
-  match l with
-  | (cons ?x ?tl) => bin_list_fold_left fcons ltac:(fcons x fnil) tl
-  | (nil _) => fnil
-  end.
-
-Ltac bin_list_iter f l :=
-  match l with
-  | (cons ?x ?tl) => f x; bin_list_iter f tl
-  | (nil _) => idtac
+Ltac OnEquation req :=
+  match goal with
+  | |- req ?lhs ?rhs => (fun f => f lhs rhs)
+  | _ => fail 1 "Goal is not an equation (of expected equality)"
   end.
- 
-(** A tactic that reverses a list *)
-Ltac Trev R l :=  
-  let rec rev_append rev l :=
-   match l with
-   | (nil _) => constr:(rev)
-   | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t 
-   end in
- rev_append (nil R) l.
 
-(* to avoid conflicts with Coq booleans*)
+Ltac ApplyLemmaAndSimpl tac lemma pe:=
+  let npe := fresh "ast_nf" in
+  let H := fresh "eq_nf" in
+  let Heq := fresh "thm" in
+  let npe_spec :=
+    match type of (lemma pe) with
+      forall (npe:_), ?npe_spec = npe -> _ => npe_spec
+    | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression"
+    end in
+  (compute_assertion H npe npe_spec;
+   (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
+   clear H;
+   tac Heq;
+   rewrite Heq; clear Heq npe).
+
+(* General scheme of reflexive tactics using of correctness lemma
+   that involves normalisation of one expression *)
+Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl :=
+  let R := match type of req with ?R -> _ => R end in
+  (* build the atom list *)
+  let fv := list_fold_left FV_tac (@List.nil R) rl in
+  (* some type-checking to avoid late errors *)
+  (check_fv fv;
+   (* rewrite steps *)
+   list_iter
+     ltac:(fun r =>
+       let ast := SYN_tac r fv in
+       (try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast))
+     rl).
+
+(********************************************************)
+
+(* An object to return when an expression is not recognized as a constant *)
 Definition NotConstant := false.
- 		       
-Ltac IN a l :=
- match l with
- | (cons a ?l) => true
- | (cons _ ?l) => IN a l
- | (nil _) => false
- end.
-
-Ltac AddFv a l :=
- match (IN a l) with
- | true => l
- | _ => constr:(cons a l)
- end.
-
-Ltac Find_at a l :=
- match l with
- | (nil _) => fail 1 "ring anomaly"
- | (cons a _) => constr:1%positive
- | (cons _ ?l) => let p := Find_at a l in eval compute in (Psucc p)
- end.
 		      
+(* Building the atom list of a ring expression *)
 Ltac FV Cst add mul sub opp t fv :=
  let rec TFV t fv :=
   match Cst t with
@@ -80,13 +67,13 @@ Ltac FV Cst add mul sub opp t fv :=
       | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (opp ?t1) => TFV t1 fv
-      | _ => AddFv t fv
+      | _ => AddFvTail t fv
       end
   | _ => fv
-  end 
+  end
  in TFV t fv.
 
- (* syntaxification *)
+ (* syntaxification of ring expressions *)
  Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := 
  let rec mkP t :=
     match Cst t with
@@ -111,67 +98,45 @@ Ltac FV Cst add mul sub opp t fv :=
  in mkP t.
 
 (* ring tactics *)
-Ltac Make_ring_rewrite_step lemma pe:=
-  let npe := fresh "npe" in
-  let H := fresh "eq_npe" in
-  let Heq := fresh "ring_thm" in
-  let npe_spec :=
-    match type of (lemma pe) with
-      forall (npe:_), ?npe_spec = npe -> _ => npe_spec
-    | _ => fail 1 "cannot find norm expression"
-    end in
-  (compute_assertion' H  npe npe_spec;
-   assert (Heq:=lemma _ _ H); clear H;
-   protect_fv in Heq;
-   (rewrite Heq; clear Heq npe) || clear npe).
-
-
-Ltac Make_ring_rw_list Cst_tac lemma req rl :=
-  match type of lemma with
-    forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C),
-    _ = npe ->
-    req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
-  let mkFV := FV Cst_tac add mul sub opp in
-  let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-  (* build the atom list *)
-  let rfv := bin_list_fold_left mkFV (nil R) rl in
-  let fv := Trev R rfv in
-  (* rewrite *)
-  bin_list_iter
-    ltac:(fun r =>
-      let pe := mkPol r fv in
-      Make_ring_rewrite_step (lemma fv) pe)
-    rl
-  | _ => fail 1 "bad lemma"
-  end.
-
-Ltac Make_ring_rw Cst_tac lemma req r :=
-  Make_ring_rw_list Cst_tac lemma req (cons r (nil _)).
-
- (* Building the generic tactic *)
 
- Ltac Make_ring_tac Cst_tac lemma1 lemma2 req :=
-  match type of lemma2 with
-    forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C),
-    _ = npe ->
-    req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
-  match goal with
-  | |- req ?r1 ?r2 =>
-    let mkFV := FV Cst_tac add mul sub opp in
-    let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-    let rfv := mkFV (add r1 r2) (nil R) in
-    let fv := Trev R rfv in
-    let pe1 := mkPol r1 fv in
-    let pe2 := mkPol r2 fv in
-    ((apply (lemma1 fv pe1 pe2);
-      vm_compute;
-      exact (refl_equal true)) ||
-     (Make_ring_rewrite_step (lemma2 fv) pe1;
-      Make_ring_rewrite_step (lemma2 fv) pe2))
-  | _ => fail 1 "goal is not an equality from a declared ring"
-  end
-  end.
+ Ltac Ring Cst_tac lemma1 req :=
+  let Make_tac :=
+    match type of lemma1 with
+    | forall (l:list ?R) (pe1 pe2:PExpr ?C),
+      _ = true ->
+      req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ =>
+        let mkFV := FV Cst_tac add mul sub opp in
+        let mkPol := mkPolexpr C Cst_tac add mul sub opp in
+        (fun f => f R mkFV mkPol)
+    | _ => fail 1 "ring anomaly: bad correctness lemma"
+    end in
+  let Main r1 r2 R mkFV mkPol :=
+    let fv := mkFV r1 (@List.nil R) in
+    let fv := mkFV r2 fv in
+    (check_fv fv;
+     let pe1 := mkPol r1 fv in
+     let pe2 := mkPol r2 fv in
+     (apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring");
+     vm_compute;
+     (exact (refl_equal true) || fail "not a valid ring equation")) in
+  Make_tac ltac:(OnEquation req Main).
+
+Ltac Ring_simplify Cst_tac lemma2 req rl :=
+  let Make_tac :=
+    match type of lemma2 with 
+      forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C),
+      _ = npe ->
+      req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
+      let mkFV := FV Cst_tac add mul sub opp in
+      let mkPol := mkPolexpr C Cst_tac add mul sub opp in
+      let simpl_ring H := protect_fv "ring" in H in
+      (fun tac => tac mkFV mkPol simpl_ring lemma2 req rl)
+    | _ => fail 1 "ring anomaly: bad correctness lemma"
+    end in
+  Make_tac ReflexiveRewriteTactic.
 
+(* A simple macro tactic to be prefered to ring_simplify *)
+Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
 
 (* coefs belong to the same type as the target ring (concrete ring) *)
 Definition ring_id_correct
@@ -183,14 +148,7 @@ Definition ring_id_correct
 
 Definition ring_rw_id_correct
   R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok :=
-  @Pphi_dev_ok  R rO rI radd rmul rsub ropp req rSet req_th ARth
-                R rO rI radd rmul rsub ropp reqb
-               (@IDphi R)
-               (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok).
-
-Definition ring_rw_id_correct'
-  R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok :=
-  @Pphi_dev_ok'  R rO rI radd rmul rsub ropp req rSet req_th ARth
+  @Pphi_dev_ok   R rO rI radd rmul rsub ropp req rSet req_th ARth
                  R rO rI radd rmul rsub ropp reqb
                 (@IDphi R)
                 (@IDmorph R rO rI radd rmul rsub ropp req rSet reqb reqb_ok).
@@ -204,551 +162,3 @@ Definition ring_rw_id_eq_correct
  @ring_rw_id_correct R rO rI radd rmul rsub ropp (@eq R)
     (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok.
 
-Definition ring_rw_id_eq_correct'
-   R rO rI radd rmul rsub ropp ARth reqb reqb_ok :=
- @ring_rw_id_correct' R rO rI radd rmul rsub ropp (@eq R)
-    (Eqsth R) (Eq_ext _ _ _) ARth reqb reqb_ok.
-
-(*
-Require Import ZArith.
-Require Import Setoid.
-Require Import Ring_tac.
-Import BinList.
-Import Ring_th.
-Open Scope Z_scope.
-
-Add New Ring Zr : (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth)
-  Computational Zeqb_ok
-  Constant Zcst.
-
-Goal forall a b, (a+b*2)*(a+b*2)=1.
-intros.
- setoid ring ((a + b * 2) * (a + b * 2)).
-
-  Make_ring_rw_list Zcst
-    (ring_rw_id_correct' (Eqsth Z) (Eq_ext _ _ _)
-      (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok)
-    (eq (A:=Z))
-   (cons ((a+b)*(a+b)) (nil _)).
-
-
-Goal forall a b, (a+b)*(a+b)=1.
-intros.
-Ltac zringl :=
-  Make_ring_rw3_list ltac:(inv_gen_phiZ 0 1 Zplus Zmult Zopp)
-    (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _)
-      (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok)
-    (eq (A:=Z))
-(BinList.cons ((a+b)*(a+b)) (BinList.nil _)).
-
-Open Scope Z_scope.
-
-let Cst_tac := inv_gen_phiZ 0 1 Zplus Zmult Zopp in
-let lemma :=
-    constr:(ring_rw_id_correct' (Eqsth Z) (Eq_ext _ _ _)
-             (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in
-let req := constr:(eq (A:=Z)) in
-let rl := constr:(cons ((a+b)*(a+b)) (nil _)) in
-Make_ring_rw_list Cst_tac lemma req rl.
-
-let fv := constr:(cons a (cons b (nil _))) in
-let pe :=
-  constr:(PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) in
-Make_ring_rewrite_step (lemma fv) pe.
-
-
-
-
-OK
-
-Lemma L0 :
- forall (l : list Z) (pe : PExpr Z) pe',
-       pe' = norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe ->
-       PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe =
-       Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe'.
-intros;  subst pe'.
-apply
- (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _)
-    (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok).
-Qed.
-Lemma L0' :
- forall (l : list Z) (pe : PExpr Z) pe',
-       norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe = pe' ->
-       PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe =
-       Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe'.
-intros;  subst pe'.
-apply
- (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _)
-    (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok).
-Qed.
-
-pose (pe:=PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))).
-compute_assertion ipattern:H (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe).
-let fv := constr:(cons a (cons b (nil _))) in
-assert (Heq := L0 fv _ (sym_equal H)); clear H.
- protect_fv' in Heq.
- rewrite Heq; clear Heq; clear pe.
-
-
-MIEUX (mais taille preuve = taille de pe + taille de nf(pe)... ):
-
-
-Lemma L :
- forall (l : list Z) (pe : PExpr Z) pe' (x y :Z),
-       pe' = norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe ->
-       x = PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe ->
-       y = Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe' ->
-       x=y.
-intros;  subst x y pe'.
-apply
- (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _)
-    (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok).
-Qed.
-Lemma L' :
- forall (l : list Z) (pe : PExpr Z) pe' (x y :Z),
-       Peq Zeq_bool pe'  (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool pe) = true ->
-       x = PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) l pe ->
-       y = Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) l pe' ->
-       forall (P:Z->Type), P y -> P x.
-intros.
- rewrite L with (2:=H0) (3:=H1); trivial.
-apply (Peq_ok (Eqsth Z) (Eq_ext _ _ _)
-   (IDmorph 0 1 Zplus Zminus Zmult Zopp (Eqsth Z) Zeq_bool Zeqb_ok) ).
-
-  (IDmorph (Eqsth Z) (Eq_ext _ _ _) Zeqb_ok).
-
-
-    (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth)).
-Qed.
-
-eapply L'
- with (x:=(a+b)*(a+b))
-      (pe:=PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)))
-      (l:=cons a (cons b (nil Z)));[compute;reflexivity|reflexivity|idtac|idtac];norm_evars;[protect_fv';reflexivity|idtac];norm_evars.
-
-
-
-
-
-set (x:=a).
-set (x0:=b).
-set (fv:=cons x (cons x0 (nil Z))).
-let fv:=constr:(cons a (cons b (nil Z))) in
-let lemma := constr : (ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _)
-      (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in
-let pe :=
-  constr :  (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) in
-assert (Heq := lemma fv pe).
-set (npe:=norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool
-             (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2)))).
-fold npe in Heq.
-move npe after fv.
-let fv' := eval red in fv in
-compute in npe.
-subst npe.
-let fv' := eval red in fv in
-compute_without_globals_of (fv',Zplus,0,1,Zmult,Zopp,Zminus) in Heq.
-rewrite Heq.
-clear Heq fv; subst x x0.
-
-
-simpl in Heq.
-unfold Pphi_dev in Heq.
-unfold mult_dev in Heq.
-unfold P0, Peq in *.
-unfold Zeq_bool at 3, Zcompare, Pcompare in Heq.
-unfold fv, hd, tl in Heq.
-unfold powl, rev, rev_append in Heq.
-unfold mkmult1 in Heq.
-unfold mkmult in Heq.
-unfold add_mult_dev in |- *.
-unfold add_mult_dev at 2 in Heq.
-unfold P0, Peq at 1 in Heq.
-unfold Zeq_bool at 2 3 4 5 6, Zcompare, Pcompare in Heq.
-unfold hd, powl, rev, rev_append in Heq.
-unfold mkadd_mult in Heq.
-unfold mkmult in Heq.
-unfold add_mult_dev in Heq.
-unfold P0, Peq in Heq.
-unfold Zeq_bool, Zcompare, Pcompare in Heq.
-unfold hd,powl, rev,rev_append in Heq.
-unfold mkadd_mult in Heq.
-unfold mkmult in Heq.
-unfold IDphi in Heq.
-
- fv := cons x (cons x0 (nil Z))
- PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))
- Heq : PEeval 0 Zplus Zmult Zminus Zopp (IDphi (R:=Z)) fv
-          (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))) =
-        Pphi_dev 0 1 Zplus Zmult 0 1 Zeq_bool (IDphi (R:=Z)) fv
-          (norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool
-             (PEmul (PEadd (PEX Z 1) (PEX Z 2)) (PEadd (PEX Z 1) (PEX Z 2))))
-
-
-
-let Cst_tac := inv_gen_phiZ 0 1 Zplus Zmult Zopp in
-let lemma :=
-    constr:(ring_rw_id_correct (Eqsth Z) (Eq_ext _ _ _)
-             (Rth_ARth (Eqsth Z) (Eq_ext _ _ _) Zth) Zeq_bool Zeqb_ok) in
-let req := constr:(eq (A:=Z)) in
-let rl := constr:(BinList.cons ((a+b)*(a+b)) (BinList.nil _)) in
-  match type of lemma with
-    forall (l:list ?R) (pe:PExpr ?C),
-    req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
-  Constant natcst.
-
-
-Require Import Setoid.
-Open Scope nat_scope.
-
-Require Import Ring_th.
-Require Import Arith.
-
-Add New Ring natr : (SRth_ARth (Eqsth nat) natSRth)
-  Computational nateq_ok
-  Constant natcst.
-
-
-Require Import Rbase.
-Open Scope R_scope.	      
-
- Lemma Rth : ring_theory 0 1 Rplus Rmult Rminus Ropp (@eq R).
- Proof.
-  constructor. exact Rplus_0_l. exact Rplus_comm. 
-  intros;symmetry;apply Rplus_assoc.
-  exact Rmult_1_l. exact Rmult_comm. 
-  intros;symmetry;apply Rmult_assoc.
-  exact Rmult_plus_distr_r. trivial. exact Rplus_opp_r.
- Qed.
-
-Add New Ring Rr : Rth Abstract.
-
-Goal forall a b, (a+b*10)*(a+b*10)=1.
-intros.
-
-Module Zring.
-  Import Zpol.
-  Import BinPos.
-  Import BinInt.
-
-Ltac is_PCst p :=
- match p with
- | xH => true
- | (xO ?p') => is_PCst p'
- | (xI ?p') => is_PCst p'
- | _ => false
- end.
-
-Ltac ZCst t :=
- match t with
- | Z0 => constr:t 
- | (Zpos ?p) =>
-    match (is_PCst p) with
-    | false => NotConstant
-    | _ => constr:t
-    end
- | (Zneg ?p) =>
-    match (is_PCst p) with
-    | false => NotConstant
-    | _ => constr:t
-    end
- | _ => NotConstant
- end.
-		  
-Ltac zring := 
-  Make_ring_tac ZCst
-    (Zpol.ring_gen_eq_correct Zth) (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z).
-
-Ltac zrewrite :=
-  Make_ring_rw3 ZCst (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z).
-
-Ltac zrewrite_list :=
-  Make_ring_rw3_list ZCst (Zpol.ring_rw_gen_eq_correct Zth) (@eq Z).
-
-End Zring.
-*)
-
-
-
-(*
-(*** Intanciation for Z*)
-Require Import ZArith.
-Open Scope Z_scope.
-
-Module Zring.
-  Let R := Z.
-  Let rO := 0.
-  Let rI := 1.
-  Let radd := Zplus.
-  Let rmul := Zmult.
-  Let rsub := Zminus.
-  Let ropp := Zopp.
-  Let Rth := Zth.
-  Let reqb := Zeq_bool.
-  Let req_morph := Zeqb_ok.
-
-  (* CE_Entries *)
-  Let C := R.
-  Let cO := rO.
-  Let cI := rI.
-  Let cadd := radd.
-  Let cmul := rmul.
-  Let csub := rsub.
-  Let copp := ropp.
-  Let req := (@eq R). 
-  Let ceqb := reqb.
-  Let phi := @IDphi R.
-  Let Rsth : Setoid_Theory R req := Eqsth R.
-  Let Reqe : ring_eq_ext radd rmul ropp req :=
-   (@Eq_ext R radd rmul ropp).
-  Let ARth : almost_ring_theory rO rI radd rmul rsub ropp req :=
-   (@Rth_ARth R rO rI radd rmul rsub ropp req Rsth Reqe Rth).
-  Let CRmorph : ring_morph rO rI radd rmul rsub ropp req
-                           cO cI cadd cmul csub copp ceqb phi :=
-   (@IDmorph R rO rI radd rmul rsub ropp req Rsth reqb req_morph).
-
-  Definition Peq := Eval red in (Pol.Peq ceqb).
-  Definition mkPinj := Eval red in (@Pol.mkPinj C). 
-  Definition mkPX :=
-   Eval red;
-        change (Pol.Peq ceqb) with Peq;
-        change (@Pol.mkPinj Z) with mkPinj in
-   (Pol.mkPX cO ceqb). 
-
-  Definition P0 := Eval red in (Pol.P0 cO).
-  Definition P1 := Eval red in (Pol.P1 cI).
-
-  Definition X :=
-   Eval red; change (Pol.P0 cO) with P0; change (Pol.P1 cI) with P1 in
-   (Pol.X cO cI).
-
-  Definition mkX :=
-   Eval red; change (Pol.X cO cI) with X in
-   (mkX cO cI).
-
-  Definition PaddC
-  Definition PaddI
-  Definition PaddX
-
-  Definition Padd :=
-   Eval red in
-        
-   (Pol.Padd cO cadd ceqb)
-
-  Definition PmulC
-  Definition PmulI
-  Definition Pmul_aux
-  Definition Pmul
-
-  Definition PsubC
-  Definition PsubI
-  Definition PsubX
-  Definition Psub
-
-
-
-  Definition norm :=
-   Eval red;
-        change (Pol.Padd cO cadd ceqb) with Padd;
-        change (Pol.Pmul cO cI cadd cmul ceqb) with Pmul;
-        change (Pol.Psub cO cadd csub copp ceqb) with Psub;
-        change (Pol.Popp copp) with Psub;
-  
- in
-   (Pol.norm cO cI cadd cmul csub copp ceqb).
-
-
-
-End Zring.
-		  
-Ltac is_PCst p :=
- match p with
- | xH => true
- | (xO ?p') => is_PCst p'
- | (xI ?p') => is_PCst p'
- | _ => false
- end.
-
-Ltac ZCst t :=
- match t with
- | Z0 => constr:t 
- | (Zpos ?p) =>
-    match (is_PCst p) with
-    | false => NotConstant
-    | _ => t
-    end
- | (Zneg ?p) =>
-    match (is_PCst p) with
-    | false => NotConstant
-    | _ => t
-    end
- | _ => NotConstant
- end.
-		  
-Ltac zring := 
-  Zring.Make_ring_tac Zplus Zmult Zminus Zopp (@eq Z) ZCst.
-
-Ltac zrewrite :=
-  Zring.Make_ring_rw3 Zplus Zmult Zminus Zopp ZCst.
-*)
-
-(*	      
-(* Instanciation for Bool *)	      
-Require Import Bool.
-	      
-Module BCE.
- Definition R := bool.
- Definition rO := false.
- Definition rI := true.
- Definition radd := xorb.
- Definition rmul := andb.
- Definition rsub := xorb.
- Definition ropp b:bool := b.
- Lemma Rth : ring_theory rO rI radd rmul rsub ropp (@eq bool).
- Proof.
-  constructor.
-   exact false_xorb.
-   exact xorb_comm.
-   intros; symmetry  in |- *; apply xorb_assoc.
-   exact andb_true_b.
-   exact andb_comm.
-   exact andb_assoc.
-   destruct x; destruct y; destruct z; reflexivity.
-   intros; reflexivity.
-   exact xorb_nilpotent.
- Qed.
-
- Definition reqb := eqb.
- Definition req_morph := eqb_prop.
-End BCE.
-
-Module BEntries := CE_Entries BCE.
-
-Module Bring := MakeRingPol BEntries.
-
-Ltac BCst t :=
-  match t with
-   | true => true
-   | false => false
-   | _ => NotConstant
-   end.
-
-Ltac bring := 
-  Bring.Make_ring_tac xorb andb xorb (fun b:bool => b) (@eq bool) BCst.
-
-Ltac brewrite :=
-  Zring.Make_ring_rw3 Zplus Zmult Zminus Zopp ZCst.
-*)
-
-(*Module Rring.
-
-(* Instanciation for R *)	      
-Require Import Rbase.
-Open Scope R_scope.	      
-
- Lemma Rth : ring_theory 0 1 Rplus Rmult Rminus Ropp (@eq R).
- Proof.
-  constructor. exact Rplus_0_l. exact Rplus_comm. 
-  intros;symmetry;apply Rplus_assoc.
-  exact Rmult_1_l. exact Rmult_comm. 
-  intros;symmetry;apply Rmult_assoc.
-  exact Rmult_plus_distr_r. trivial. exact Rplus_opp_r.
- Qed.
-
-Ltac RCst := inv_gen_phiZ 0 1 Rplus Rmul Ropp.
-
-Ltac rring :=
-  Make_ring_tac RCst
-    (Zpol.ring_gen_eq_correct Rth) (Zpol.ring_rw_gen_eq_correct Rth) (@eq R).
-
-Ltac rrewrite :=
-  Make_ring_rw3 RCst (Zpol.ring_rw_gen_eq_correct Rth) (@eq R).
-
-Ltac rrewrite_list :=
-  Make_ring_rw3_list RCst (Zpol.ring_rw_gen_eq_correct Rth) (@eq R).
-
-End Rring.
-*)
-(************************)
-(*
-(* Instanciation for N *)	     
-Require Import NArith.
-Open Scope N_scope.
-		
-Module NCSE.
- Definition R := N.
- Definition rO := 0.
- Definition rI := 1.
- Definition radd := Nplus.
- Definition rmul := Nmult.
- Definition SRth := Nth.
- Definition reqb := Neq_bool.
- Definition req_morph := Neq_bool_ok.
-End NCSE.
-
-Module NEntries := CSE_Entries NCSE.
-
-Module Nring := MakeRingPol NEntries.
-
-Ltac NCst := inv_gen_phiN 0 1 Nplus Nmult.
-
-Ltac nring :=  
-  Nring.Make_ring_tac Nplus Nmult (@SRsub N Nplus) (@SRopp N) (@eq N) NCst.
-
-Ltac nrewrite :=
-  Nring.Make_ring_rw3 Nplus Nmult  (@SRsub N Nplus) (@SRopp N) NCst.
-	       
-(* Instanciation for nat *)	       
-Open Scope nat_scope.
-
-Module NatASE.
- Definition R := nat.
- Definition rO := 0.
- Definition rI := 1.
- Definition radd := plus.
- Definition rmul := mult.
- Lemma SRth : semi_ring_theory O (S O) plus mult (@eq nat).
- Proof.
-  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
-  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
-  exact mult_plus_distr_r. 
- Qed.
-End NatASE.
-
-Module NatEntries := ASE_Entries NatASE.
-
-Module Natring := MakeRingPol NatEntries.
-
-Ltac natCst t := 
- match t with
- | O => N0
- | (S ?n) =>
-    match (natCst n) with
-    | NotConstant => NotConstant
-    | ?p => constr:(Nsucc p)
-    end
- | _ => NotConstant
- end.
-		  
-Ltac natring :=
- Natring.Make_ring_tac plus mult (@SRsub nat plus) (@SRopp nat) (@eq nat) natCst.
-
-Ltac natrewrite :=
-  Natring.Make_ring_rw3 plus mult (@SRsub nat plus) (@SRopp nat) natCst.
-	  
-(* Generic tactic, checks the type of the terms and applies the
-suitable instanciation*)
-		  
-Ltac newring :=  
- match goal with
- | |- (?r1 = ?r2) =>
-   match (type of r1) with
-   | Z => zring
-   | R => rring
-   | bool => bring
-   | N => nring
-   | nat => natring
-   end
- end.
-
-*)
diff --git a/contrib/setoid_ring/Ring_th.v b/contrib/setoid_ring/Ring_th.v
index 9583dd2d9..a7dacaa75 100644
--- a/contrib/setoid_ring/Ring_th.v
+++ b/contrib/setoid_ring/Ring_th.v
@@ -1,7 +1,15 @@
-Require Import Setoid.
- Set Implicit Arguments.
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
+Require Import Setoid.
+Set Implicit Arguments.
 
+Module RingSyntax.
 Reserved Notation "x ?=! y" (at level 70, no associativity).
 Reserved Notation "x +! y " (at level 50, left associativity).
 Reserved Notation "x -! y" (at level 50, left associativity).
@@ -17,8 +25,8 @@ Reserved Notation "x ** y" (at level 40, left associativity).
 Reserved Notation "-- x" (at level 35, right associativity).
 
 Reserved Notation "x == y" (at level 70, no associativity).
-
-
+End RingSyntax.
+Import RingSyntax.
 
 Section DEFINITIONS.
  Variable R : Type.
@@ -42,7 +50,7 @@ Section DEFINITIONS.
   }.
   
  (** Almost Ring *)
-(*Almost ring are no ring : Ropp_def is missi**)
+(*Almost ring are no ring : Ropp_def is missing **)
  Record almost_ring_theory : Prop := mk_art {
     ARadd_0_l   : forall x, 0 + x == x;
     ARadd_sym   : forall x y, x + y == y + x;
@@ -343,6 +351,12 @@ Section ALMOST_RING.
  (** Usefull lemmas on almost ring *)
  Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
 
+ Lemma ARth_SRth : semi_ring_theory 0 1 radd rmul req.
+Proof.
+elim ARth; intros.
+constructor; trivial.
+Qed.
+
  Lemma ARsub_ext :
       forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
  Proof.
diff --git a/contrib/setoid_ring/ZRing_th.v b/contrib/setoid_ring/ZRing_th.v
index 9060428b9..08eb54aa8 100644
--- a/contrib/setoid_ring/ZRing_th.v
+++ b/contrib/setoid_ring/ZRing_th.v
@@ -1,11 +1,20 @@
-Require Import Ring_th.
-Require Import Pol.
-Require Import Ring_tac.
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import ZArith_base.
 Require Import BinInt.
 Require Import BinNat.
 Require Import Setoid.
- Set Implicit Arguments.
+Require Import Ring_base.
+Require Import Pol.
+Set Implicit Arguments.
+
+Import RingSyntax.
 
 (** Z is a ring and a setoid*)
 
@@ -255,6 +264,14 @@ Lemma Neq_bool_ok : forall x y, Neq_bool x y = true -> x = y.
   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.
+
 (**Same as above : definition of two,extensionaly equal, generic morphisms *)
 (**from N to any semi-ring*)
 Section NMORPHISM.
@@ -326,271 +343,9 @@ Section NMORPHISM.
  Qed.
 
 End NMORPHISM.
-(*
-Section NNMORPHISM.
-Variable R : Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
-  Variable Rsth : Setoid_Theory R req.
-     Add Setoid R req Rsth as R_setoid5.
-     Ltac rrefl := gen_reflexivity Rsth.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
-   Add Morphism radd : radd_ext5.  exact Reqe.(Radd_ext). Qed.
-   Add Morphism rmul : rmul_ext5.  exact Reqe.(Rmul_ext). Qed.
-   Add Morphism ropp : ropp_ext5.  exact Reqe.(Ropp_ext). Qed.
-
- Lemma SReqe : sring_eq_ext radd rmul req.
-  case Reqe; constructor; trivial.
- Qed.
-
- Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
-   Add Morphism rsub : rsub_ext6. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
-   Ltac add_push := gen_add_push radd Rsth Reqe ARth.
-
- Lemma SRth : semi_ring_theory 0 1 radd rmul req. 
-  case ARth; constructor; trivial.
- Qed.
-
-  Definition NN := prod N N.
-  Definition gen_phiNN (x:NN) :=
-    rsub (gen_phiN rO rI radd rmul (fst x)) (gen_phiN rO rI radd rmul (snd x)).
-  Notation "[ x ]" := (gen_phiNN x).   
-
-  Definition NNadd (x y : NN) : NN :=
-    (fst x + fst y, snd x + snd y)%N.
-  Definition NNmul (x y : NN) : NN :=
-    (fst x * fst y + snd x * snd y, fst y * snd x + fst x * snd y)%N.
-  Definition NNopp (x:NN) : NN := (snd x, fst x)%N.
-  Definition NNsub (x y:NN) : NN := (fst x + snd y, fst y + snd x)%N.
-
-
- Lemma gen_phiNN_add : forall x y, [NNadd x y] == [x] + [y].
- Proof.
-intros.
-unfold NNadd, gen_phiNN in |- *; simpl in |- *.
-repeat  rewrite (gen_phiN_add Rsth SReqe SRth).
-norm.
-add_push (- gen_phiN 0 1 radd rmul (snd x)).
-rrefl.
-Qed.
- 
-  Hypothesis ropp_involutive : forall x, - - x == x.
-
-
- Lemma gen_phiNN_mult : forall x y, [NNmul x y] == [x] * [y].
- Proof.
-intros.
-unfold NNmul, gen_phiNN in |- *; simpl in |- *.
-repeat  rewrite (gen_phiN_add Rsth SReqe SRth).
-repeat  rewrite (gen_phiN_mult Rsth SReqe SRth).
-norm.
-rewrite ropp_involutive.
-add_push (- (gen_phiN 0 1 radd rmul (fst y) * gen_phiN 0 1 radd rmul (snd x))).
-add_push ( gen_phiN 0 1 radd rmul (snd x) * gen_phiN 0 1 radd rmul (snd y)).
-rewrite (ARmul_sym ARth (gen_phiN 0 1 radd rmul (fst y))
-            (gen_phiN 0 1 radd rmul (snd x))).
-rrefl.
-Qed.
-
- Lemma gen_phiNN_sub : forall x y, [NNsub x y] == [x] - [y].
-intros.
-unfold NNsub, gen_phiNN; simpl.
-repeat rewrite (gen_phiN_add Rsth SReqe SRth).
-repeat rewrite (ARsub_def ARth).
-repeat rewrite (ARopp_add ARth).
-repeat rewrite (ARadd_assoc ARth).
-rewrite ropp_involutive.
-add_push (- gen_phiN 0 1 radd rmul (fst y)).
-add_push ( - gen_phiN 0 1 radd rmul (snd x)).
-rrefl.
-Qed.
-
-
-Definition NNeqbool (x y: NN) :=
-  andb (Neq_bool (fst x) (fst y)) (Neq_bool (snd x) (snd y)).
-
-Lemma NNeqbool_ok0 : forall x y,
-  NNeqbool x y = true -> x = y.
-unfold NNeqbool in |- *.
-intros.
-assert (Neq_bool (fst x) (fst y) = true).
- generalize H.
-   case (Neq_bool (fst x) (fst y)); simpl in |- *; trivial.
- assert (Neq_bool (snd x) (snd y) = true).
-   rewrite H0 in H; simpl in |- *; trivial.
-  generalize H0 H1.
-    destruct x; destruct y; simpl in |- *.
-    intros.
-     replace n with n1.
-    replace n2 with n0; trivial.
-     apply Neq_bool_ok; trivial.
-   symmetry  in |- *.
-     apply Neq_bool_ok; trivial.
-Qed.
-
-
-(*gen_phiN satisfies morphism specifications*)
- Lemma gen_phiNN_morph : ring_morph 0 1 radd rmul rsub ropp req
-                        (N0,N0) (Npos xH,N0) NNadd NNmul NNsub NNopp NNeqbool gen_phiNN.
- 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.
- Qed.
-
-End NNMORPHISM.
-
-Section NSTARMORPHISM.
-Variable R : Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
-  Variable Rsth : Setoid_Theory R req.
-     Add Setoid R req Rsth as R_setoid3.
-     Ltac rrefl := gen_reflexivity Rsth.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
-   Add Morphism radd : radd_ext3.  exact Reqe.(Radd_ext). Qed.
-   Add Morphism rmul : rmul_ext3.  exact Reqe.(Rmul_ext). Qed.
-   Add Morphism ropp : ropp_ext3.  exact Reqe.(Ropp_ext). Qed.
-
- Lemma SReqe : sring_eq_ext radd rmul req.
-  case Reqe; constructor; trivial.
- Qed.
-
- Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
-   Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
-   Ltac add_push := gen_add_push radd Rsth Reqe ARth.
-
- Lemma SRth : semi_ring_theory 0 1 radd rmul req. 
-  case ARth; constructor; trivial.
- Qed.
-
-  Inductive Nword : Set :=
-    Nlast (p:positive)
-  | Ndigit (n:N) (w:Nword).
-
-  Fixpoint opp_iter (n:nat) (t:R) {struct n} : R :=
-    match n with 
-      O => t
-    | S k => ropp (opp_iter k t)
-    end.
-
-  Fixpoint gen_phiNword (x:Nword) (n:nat) {struct x} : R :=
-    match x with
-      Nlast p => opp_iter n (gen_phi_pos p)
-    | Ndigit N0 w => gen_phiNword w (S n)
-    | Ndigit m w => radd (opp_iter n (gen_phiN m)) (gen_phiNword w (S n))
-    end.
-  Notation "[ x ]" := (gen_phiNword x).   
-
-  Fixpoint Nwadd (x y : Nword) {struct x} : Nword :=
-    match x, y with
-      Nlast p1, Nlast p2 => Nlast (p1+p2)%positive
-    | Nlast p1, Ndigit n w => Ndigit (Npos p1 + n)%N w
-    | Ndigit n w, Nlast p1 => Ndigit (n + Npos p1)%N w
-    | Ndigit n1 w1, Ndigit n2 w2 => Ndigit (n1+n2)%N (Nwadd w1 w2)
-    end.
-  Fixpoint Nwmulp (x:positive) (y:Nword) {struct y} : Nword :=
-    match y with
-      Nlast p => Nlast (x*p)%positive
-    | Ndigit n w => Ndigit (Npos x * n)%N (Nwmulp x w)
-    end.
-  Definition Nwmul (x y : Nword) {struct x} : Nword :=
-    match x with
-      Nlast k => Nmulp k y
-    | Ndigit N0 w => Ndigit N0 (Nwmul w y)
-    | Ndigit (Npos k) w =>
-        Nwadd (Nwmulp k y) (Ndigit N0 (Nwmul w y))
-   end.
-
-  Definition Nwopp (x:Nword) : Nword := Ndigit N0 x.
-  Definition Nwsub (x y:NN) : NN := (Nwadd x (Ndigit N0 y)).
-
-
- Lemma gen_phiNN_add : forall x y, [NNadd x y] == [x] + [y].
- Proof.
-intros.
-unfold NNadd, gen_phiNN in |- *; simpl in |- *.
-repeat  rewrite (gen_phiN_add Rsth SReqe SRth).
-norm.
-add_push (- gen_phiN 0 1 radd rmul (snd x)).
-rrefl.
-Qed.
-
- Lemma gen_phiNN_mult : forall x y, [NNmul x y] == [x] * [y].
- Proof.
-intros.
-unfold NNmul, gen_phiNN in |- *; simpl in |- *.
-repeat  rewrite (gen_phiN_add Rsth SReqe SRth).
-repeat  rewrite (gen_phiN_mult Rsth SReqe SRth).
-norm.
-rewrite ropp_involutive.
-add_push (- (gen_phiN 0 1 radd rmul (fst y) * gen_phiN 0 1 radd rmul (snd x))).
-add_push ( gen_phiN 0 1 radd rmul (snd x) * gen_phiN 0 1 radd rmul (snd y)).
-rewrite (ARmul_sym ARth (gen_phiN 0 1 radd rmul (fst y))
-            (gen_phiN 0 1 radd rmul (snd x))).
-rrefl.
-Qed.
-
- Lemma gen_phiNN_sub : forall x y, [NNsub x y] == [x] - [y].
-intros.
-unfold NNsub, gen_phiNN; simpl.
-repeat rewrite (gen_phiN_add Rsth SReqe SRth).
-repeat rewrite (ARsub_def ARth).
-repeat rewrite (ARopp_add ARth).
-repeat rewrite (ARadd_assoc ARth).
-rewrite ropp_involutive.
-add_push (- gen_phiN 0 1 radd rmul (fst y)).
-add_push ( - gen_phiN 0 1 radd rmul (snd x)).
-rrefl.
-Qed.
-
-
-Definition NNeqbool (x y: NN) :=
-  andb (Neq_bool (fst x) (fst y)) (Neq_bool (snd x) (snd y)).
-
-Lemma NNeqbool_ok0 : forall x y,
-  NNeqbool x y = true -> x = y.
-unfold NNeqbool in |- *.
-intros.
-assert (Neq_bool (fst x) (fst y) = true).
- generalize H.
-   case (Neq_bool (fst x) (fst y)); simpl in |- *; trivial.
- assert (Neq_bool (snd x) (snd y) = true).
-   rewrite H0 in H; simpl in |- *; trivial.
-  generalize H0 H1.
-    destruct x; destruct y; simpl in |- *.
-    intros.
-     replace n with n1.
-    replace n2 with n0; trivial.
-     apply Neq_bool_ok; trivial.
-   symmetry  in |- *.
-     apply Neq_bool_ok; trivial.
-Qed.
-
-
-(*gen_phiN satisfies morphism specifications*)
- Lemma gen_phiNN_morph : ring_morph 0 1 radd rmul rsub ropp req
-                        (N0,N0) (Npos xH,N0) NNadd NNmul NNsub NNopp NNeqbool gen_phiNN.
- 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.
- Qed.
-
-End NSTARMORPHISM.
-*)
 
- (* syntaxification of constants in an abstract ring *)
+ (* syntaxification of constants in an abstract ring:
+    the inverse of gen_phiPOS *)
  Ltac inv_gen_phi_pos rI add mul t :=
    let rec inv_cst t :=
    match t with
@@ -600,7 +355,7 @@ End NSTARMORPHISM.
    | (mul (add rI rI) ?p) => (* 2p *)
        match inv_cst p with
          NotConstant => NotConstant
-       | 1%positive => NotConstant
+       | 1%positive => NotConstant (* 2*1 is not convertible to 2 *)
        | ?p => constr:(xO p)
        end
    | (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
@@ -613,6 +368,7 @@ End NSTARMORPHISM.
    end in
    inv_cst t.
 
+(* The inverse of gen_phiN *)
  Ltac inv_gen_phiN rO rI add mul t :=
    match t with
      rO => constr:0%N
@@ -623,6 +379,7 @@ End NSTARMORPHISM.
      end
    end.
 
+(* The inverse of gen_phiZ *)
  Ltac inv_gen_phiZ rO rI add mul opp t :=
    match t with
      rO => constr:0%Z
@@ -637,6 +394,7 @@ End NSTARMORPHISM.
      | ?p => constr:(Zpos p)
      end
    end.
+
 (* coefs = Z (abstract ring) *)
 Module Zpol.
 
@@ -650,15 +408,7 @@ Definition ring_gen_correct
 
 Definition ring_rw_gen_correct
   R rO rI radd rmul rsub ropp req rSet req_th Rth :=
-  @Pphi_dev_ok  R rO rI radd rmul rsub ropp req rSet req_th
-                (Rth_ARth rSet req_th Rth)
-                Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
-                (@gen_phiZ R rO rI radd rmul ropp)
-            (@gen_phiZ_morph R rO rI radd rmul rsub ropp req rSet req_th Rth).
-
-Definition ring_rw_gen_correct'
-  R rO rI radd rmul rsub ropp req rSet req_th Rth :=
-  @Pphi_dev_ok'  R rO rI radd rmul rsub ropp req rSet req_th
+  @Pphi_dev_ok   R rO rI radd rmul rsub ropp req rSet req_th
                  (Rth_ARth rSet req_th Rth)
                  Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
                  (@gen_phiZ R rO rI radd rmul ropp)
@@ -672,10 +422,6 @@ Definition ring_rw_gen_eq_correct R rO rI radd rmul rsub ropp Rth :=
   @ring_rw_gen_correct
      R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth.
 
-Definition ring_rw_gen_eq_correct' R rO rI radd rmul rsub ropp Rth :=
-  @ring_rw_gen_correct'
-     R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth.
-
 End Zpol.
 
 (* coefs = N (abstract semi-ring) *)
@@ -692,16 +438,7 @@ Definition ring_gen_correct
 
 Definition ring_rw_gen_correct
   R rO rI radd rmul req rSet req_th SRth :=
-  @Pphi_dev_ok  R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet
-                (SReqe_Reqe req_th)
-                (SRth_ARth rSet SRth)
-                N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool
-                (@gen_phiN R rO rI radd rmul)
-            (@gen_phiN_morph R rO rI radd rmul req rSet req_th SRth).
-
-Definition ring_rw_gen_correct'
-  R rO rI radd rmul req rSet req_th SRth :=
-  @Pphi_dev_ok'  R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet
+  @Pphi_dev_ok   R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet
                  (SReqe_Reqe req_th)
                  (SRth_ARth rSet SRth)
                  N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool
@@ -712,91 +449,8 @@ Definition ring_gen_eq_correct R rO rI radd rmul SRth :=
   @ring_gen_correct
      R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth.
 
-Definition ring_rw_gen_eq_correct R rO rI radd rmul SRth :=
-  @ring_rw_gen_correct
-     R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth.
-
 Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth :=
-  @ring_rw_gen_correct'
+  @ring_rw_gen_correct
      R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth.
 
 End Npol.
-
-(* Z *)
-
-Ltac isZcst t :=
-  match t with
-    Z0 => constr:true
-  | Zpos ?p => isZcst p
-  | Zneg ?p => isZcst p
-  | xI ?p => isZcst p
-  | xO ?p => isZcst p
-  | xH => constr:true
-  | _ => constr:false
-  end.
-Ltac Zcst t :=
-  match isZcst t with
-    true => t
-  | _ => NotConstant
-  end.
-
-Add New Ring Zr : Zth Computational Zeqb_ok Constant Zcst.
-
-(* N *)
-
-Ltac isNcst t :=
-  match t with
-    N0 => constr:true
-  | Npos ?p => isNcst p
-  | xI ?p => isNcst p
-  | xO ?p => isNcst p
-  | xH => constr:true
-  | _ => constr:false
-  end.
-Ltac Ncst t :=
-  match isNcst t with
-    true => t
-  | _ => NotConstant
-  end.
-
-Add New Ring Nr : Nth Computational Neq_bool_ok Constant Ncst.
-
-(* nat *)
-
-Ltac isnatcst t :=
-  match t with
-    O => true
-  | S ?p => isnatcst p
-  | _ => false
-  end.
-Ltac natcst t :=
-  match isnatcst t with
-    true => t
-  | _ => NotConstant
-  end.
-
- Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
- Proof.
-  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
-  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
-  exact mult_plus_distr_r. 
- Qed.
-
-
-Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
-  match n, m with
-  | O, O => true
-  | S n', S m' => nateq n' m'
-  | _, _ => false
-  end.
-
-Lemma nateq_ok : forall n m:nat, nateq n m = true -> n = m.
-Proof.
-  simple induction n; simple induction m; simpl; intros; try discriminate.
-  trivial.
-  rewrite (H n1 H1).
-  trivial.
-Qed.
-
-Add New Ring natr : natSRth Computational nateq_ok Constant natcst.
-
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index f35b457a5..7526cc8a6 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -16,6 +16,7 @@ open Names
 open Term
 open Closure
 open Environ
+open Libnames
 open Tactics
 open Rawterm
 open Tacticals
@@ -27,11 +28,120 @@ open Setoid_replace
 open Proof_type
 open Coqlib
 open Tacmach
-open Ppconstr
 open Mod_subst
 open Tacinterp
 open Libobject
 open Printer
+open Declare
+open Decl_kinds
+open Entries
+
+(****************************************************************************)
+(* controlled reduction *)
+
+let mark_arg i c = mkEvar(i,[|c|]);;
+let unmark_arg f c =
+  match destEvar c with
+    | (i,[|c|]) -> f i c
+    | _ -> assert false;;
+
+type protect_flag = Eval|Prot|Rec ;;
+
+let tag_arg tag_rec map i c =
+  match map i with
+      Eval -> inject c
+    | Prot -> mk_atom c
+    | Rec -> if i = -1 then inject c else tag_rec c
+
+let rec mk_clos_but f_map t =
+  match f_map t with
+    | Some map -> tag_arg (mk_clos_but f_map) map (-1) t
+    | None ->
+        (match kind_of_term t with
+            App(f,args) -> mk_clos_app_but f_map f args 0
+          | _ -> mk_atom t)
+
+and mk_clos_app_but f_map f args n =
+  if n >= Array.length args then mk_atom(mkApp(f, args))
+  else
+    let fargs, args' = array_chop n args in
+    let f' = mkApp(f,fargs) in
+    match f_map f' with
+        Some map ->
+          mk_clos_deep
+            (fun _ -> unmark_arg (tag_arg (mk_clos_but f_map) map))
+            (Esubst.ESID 0)
+            (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
+      | None -> mk_clos_app_but f_map f args (n+1)
+;;
+
+let interp_map l c =
+  try
+    let (im,am) = List.assoc c l in
+    Some(fun i ->
+      if List.mem i im then Eval
+      else if List.mem i am then Prot
+      else if i = -1 then Eval
+      else Rec)
+  with Not_found -> None
+
+let interp_map l t =
+  try Some(List.assoc t l) with Not_found -> None
+
+let protect_maps = ref ([]:(string*(constr->'a)) list)
+let add_map s m = protect_maps := (s,m) :: !protect_maps
+let lookup_map map =
+  try List.assoc map !protect_maps
+  with Not_found ->
+    errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
+
+let protect_red map env sigma c =
+  kl (create_clos_infos betadeltaiota env)
+    (mk_clos_but (lookup_map map c) 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));;
+
+
+TACTIC EXTEND protect_fv
+  [ "protect_fv" string(map) "in" ident(id) ] -> 
+    [ protect_tac_in map id ]
+| [ "protect_fv" string(map) ] -> 
+    [ protect_tac map ]
+END;;
+
+(****************************************************************************)
+
+let closed_term t l =
+  let l = List.map constr_of_global l in
+  let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
+  if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
+;;
+
+TACTIC EXTEND closed_term
+  [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
+    [ closed_term t l ]
+END
+;;
+(*
+let closed_term_ast l =
+  TacFun([Some(id_of_string"t")],
+  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
+  [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t"));
+   Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l])))
+*)
+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.wit_list1 Genarg.globwit_ref) l])))
+(*
+let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
+*)
 
 (****************************************************************************)
 (* Library linking *)
@@ -40,11 +150,15 @@ let contrib_name = "setoid_ring"
 
 
 let ring_dir = ["Coq";contrib_name]
-let setoids_dir = ["Coq";"Setoids"]
 let ring_modules = 
   [ring_dir@["BinList"];ring_dir@["Ring_th"];ring_dir@["Pol"];
-   ring_dir@["Ring_tac"];ring_dir@["ZRing_th"]]
-let stdlib_modules = [setoids_dir@["Setoid"]]
+   ring_dir@["Ring_tac"];ring_dir@["Field_tac"];ring_dir@["ZRing_th"]]
+let stdlib_modules =
+  [["Coq";"Setoids";"Setoid"];
+   ["Coq";"ZArith";"BinInt"];
+   ["Coq";"ZArith";"Zbool"];
+   ["Coq";"NArith";"BinNat"];
+   ["Coq";"NArith";"BinPos"]]
 
 let coq_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
@@ -66,23 +180,18 @@ let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
 let pol_cst s = mk_cst [contrib_name;"Pol"] s ;;
 
-let ic c =
-  let env = Global.env() and sigma = Evd.empty in
-  Constrintern.interp_constr sigma env c
-
-
 (* Ring theory *)
 
 (* almost_ring defs *)
 let coq_almost_ring_theory = ring_constant "almost_ring_theory"
 let coq_ring_lemma1 = ring_constant "ring_correct"
-let coq_ring_lemma2 = ring_constant "Pphi_dev_ok'"
+let coq_ring_lemma2 = ring_constant "Pphi_dev_ok"
 let ring_comp1 = ring_constant "ring_id_correct"
-let ring_comp2 = ring_constant "ring_rw_id_correct'"
+let ring_comp2 = ring_constant "ring_rw_id_correct"
 let ring_abs1 = ringtac_constant "Zpol" "ring_gen_correct"
-let ring_abs2 = ringtac_constant "Zpol" "ring_rw_gen_correct'"
+let ring_abs2 = ringtac_constant "Zpol" "ring_rw_gen_correct"
 let sring_abs1 = ringtac_constant "Npol" "ring_gen_correct"
-let sring_abs2 = ringtac_constant "Npol" "ring_rw_gen_correct'"
+let sring_abs2 = ringtac_constant "Npol" "ring_rw_gen_correct"
 
 (* setoid and morphism utilities *)
 let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
@@ -105,148 +214,138 @@ let coq_SRsub = ring_constant "SRsub"
 let coq_SRopp = ring_constant "SRopp"
 let coq_SReqe_Reqe = ring_constant "SReqe_Reqe"
 
-let ltac_setoid_ring = ltac"Make_ring_tac"
-let ltac_setoid_ring_rewrite = ltac"Make_ring_rw_list"
+let ltac_setoid_ring = ltac"Ring"
+let ltac_setoid_ring_rewrite = ltac"Ring_simplify"
 let ltac_inv_morphZ = zltac"inv_gen_phiZ"
 let ltac_inv_morphN = zltac"inv_gen_phiN"
 
-let coq_cons = ring_constant "cons"
-let coq_nil = ring_constant "nil"
+
+let list_dir = ["Lists";"List"]
+(* let list_dir =[contrib_name;"BinList"] *)
+let coq_cons = mk_cst list_dir "cons"
+let coq_nil = mk_cst list_dir "nil"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
 let dest_rel t =
   match kind_of_term t with
       App(f,args) when Array.length args >= 2 ->
-        mkApp(f,Array.sub args 0 (Array.length args - 2))
-    | _ -> failwith "cannot find relation"
-
-(****************************************************************************)
-(* controlled reduction *)
-
-let mark_arg i c = mkEvar(i,[|c|]);;
-let unmark_arg f c =
-  match destEvar c with
-    | (i,[|c|]) -> f i c
-    | _ -> assert false;;
-
-type protect_flag = Eval|Prot|Rec ;;
-
-let tag_arg tag_rec map i c =
-  match map i with
-      Eval -> inject c
-    | Prot -> mk_atom c
-    | Rec -> if i = -1 then inject c else tag_rec c
-
-let rec mk_clos_but f_map t =
-  match f_map t with
-    | Some map -> tag_arg (mk_clos_but f_map) map (-1) t
-    | None ->
-        (match kind_of_term t with
-            App(f,args) -> mk_clos_app_but f_map f args 0
-          (* unspecified constants are evaluated *)
-          | _ -> inject t)
-
-and mk_clos_app_but f_map f args n =
-  if n >= Array.length args then inject(mkApp(f, args))
-  else
-    let fargs, args' = array_chop n args in
-    let f' = mkApp(f,fargs) in
-    match f_map f' with
-        Some map ->
-          mk_clos_deep
-            (fun _ -> unmark_arg (tag_arg (mk_clos_but f_map) map))
-            (Esubst.ESID 0)
-            (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
-      | None -> mk_clos_app_but f_map f args (n+1)
-;;
-
-let interp_map l c =
-  try
-    let (im,am) = List.assoc c l in
-    Some(fun i ->
-      if List.mem i im then Eval
-      else if List.mem i am then Prot
-      else if i = -1 then Eval
-      else Rec)
-  with Not_found -> None
-
-let interp_map l t =
-  try Some(List.assoc t l) with Not_found -> None
-
-let arg_map =
-  [mk_cst [contrib_name;"BinList"] "cons",(function -1->Eval|2->Rec|_->Prot);
-   mk_cst [contrib_name;"BinList"] "nil", (function -1->Eval|_ -> Prot);
-   (* Pphi_dev: evaluate polynomial and coef operations, protect
-       ring operations and make recursive call on morphism and var map *)
-   pol_cst "Pphi_dev", (function -1|6|7|8|11->Eval|9|10->Rec|_->Prot);
-   (* PEeval: evaluate polynomial, protect ring operations
-      and make recursive call on morphism and var map *)
-   pol_cst "PEeval", (function -1|9->Eval|7|8->Rec|_->Prot);
-   (* Do not evaluate ring operations... *)
-   ring_constant "gen_phiZ", (function -1|6->Eval|_->Prot);
-   ring_constant "gen_phiN", (function -1|5->Eval|_->Prot);
-];;
+        (mkApp(f,Array.sub args 0 (Array.length args - 2)),
+         args.(Array.length args - 2),
+         args.(Array.length args - 1))
+    | _ -> error "ring: cannot find relation"
 
 (* Equality: do not evaluate but make recursive call on both sides *)
-let is_ring_thm req =
+let map_with_eq arg_map c =
+  let (req,_,_) = dest_rel c in
   interp_map
     ((req,(function -1->Prot|_->Rec))::
     List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
 ;;
 
-let protect_red env sigma c =
-  let req = dest_rel c in
-  kl (create_clos_infos betadeltaiota env)
-    (mk_clos_but (is_ring_thm req) c);;
+let _ = add_map "ring"
+  (map_with_eq
+    [coq_cons,(function -1->Eval|2->Rec|_->Prot);
+    coq_nil, (function -1->Eval|_ -> Prot);
+    (* Pphi_dev: evaluate polynomial and coef operations, protect
+       ring operations and make recursive call on the var map *)
+    pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot);
+    (* PEeval: evaluate morphism and polynomial, protect ring 
+       operations and make recursive call on the var map *)
+    pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot)]);;
+
+let ic c =
+  let env = Global.env() and sigma = Evd.empty in
+  Constrintern.interp_constr sigma env c
 
-let protect_tac =
-  Tactics.reduct_option (protect_red,DEFAULTcast) None ;;
+let ty c = Typing.type_of (Global.env()) Evd.empty c
 
-let protect_tac_in id =
-  Tactics.reduct_option (protect_red,DEFAULTcast) (Some(([],id),InHyp));;
+let decl_constant na c =
+  mkConst(declare_constant (id_of_string na) (DefinitionEntry 
+    { const_entry_body = c;
+      const_entry_type = None;
+      const_entry_opaque = true;
+      const_entry_boxed = true}, 
+    IsProof Lemma))
 
 
-TACTIC EXTEND protect_fv
-  [ "protect_fv" "in" ident(id) ] -> 
-    [ protect_tac_in id ]
-| [ "protect_fv" ] -> 
-    [ protect_tac ]
-END;;
+let ltac_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
 
 (****************************************************************************)
 (* Ring database *)
 
-let ty c = Typing.type_of (Global.env()) Evd.empty c
-
-
 type ring_info =
     { ring_carrier : types;
       ring_req : constr;
       ring_cst_tac : glob_tactic_expr;
       ring_lemma1 : constr;
-      ring_lemma2 : constr }
+      ring_lemma2 : constr;
+      ring_pre_tac : glob_tactic_expr;
+      ring_post_tac : glob_tactic_expr }
 
 module Cmap = Map.Make(struct type t = constr let compare = compare end)
 
 let from_carrier = ref Cmap.empty
 let from_relation = ref Cmap.empty
+let from_name = ref Spmap.empty
+
+let ring_for_carrier r = Cmap.find r !from_carrier
+let ring_for_relation rel = Cmap.find rel !from_relation
+let ring_lookup_by_name ref =
+  Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name
+
+
+let find_ring_structure env sigma l cl oname =
+  match oname, l with
+      Some rf, _ ->
+        (try ring_lookup_by_name rf
+        with Not_found ->
+          errorlabstrm "ring"
+            (str "found no ring named "++pr_reference rf))
+    | None, t::cl' ->
+        let ty = Retyping.get_type_of env sigma t in
+        let check c =
+          let ty' = Retyping.get_type_of env sigma c in
+          if not (Reductionops.is_conv env sigma ty ty') then
+            errorlabstrm "ring"
+              (str"arguments of ring_simplify do not have all the same type")
+        in
+        List.iter check cl';
+        (try ring_for_carrier ty
+        with Not_found ->
+          errorlabstrm "ring"
+            (str"cannot find a declared ring structure over"++
+             spc()++str"\""++pr_constr ty++str"\""))
+    | None, [] ->
+        let (req,_,_) = dest_rel cl in
+        (try ring_for_relation req
+        with Not_found ->
+          errorlabstrm "ring"
+            (str"cannot find a declared ring structure for equality"++
+             spc()++str"\""++pr_constr req++str"\""))
 
 let _ = 
   Summary.declare_summary "tactic-new-ring-table"
-    { Summary.freeze_function = (fun () -> !from_carrier,!from_relation);
+    { Summary.freeze_function =
+        (fun () -> !from_carrier,!from_relation,!from_name);
       Summary.unfreeze_function =
-        (fun (ct,rt) -> from_carrier := ct; from_relation := rt);
+        (fun (ct,rt,nt) ->
+          from_carrier := ct; from_relation := rt; from_name := nt);
       Summary.init_function =
-        (fun () -> from_carrier := Cmap.empty; from_relation := Cmap.empty);
+        (fun () ->
+          from_carrier := Cmap.empty; from_relation := Cmap.empty;
+          from_name := Spmap.empty);
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-let add_entry _ e =
-  let _ = ty e.ring_lemma1 in
+let add_entry (sp,_kn) e =
+(*  let _ = ty e.ring_lemma1 in
   let _ = ty e.ring_lemma2 in
+*)
   from_carrier := Cmap.add e.ring_carrier e !from_carrier;
-  from_relation := Cmap.add e.ring_req e !from_relation
+  from_relation := Cmap.add e.ring_req e !from_relation;
+  from_name := Spmap.add sp e !from_name 
 
 
 let subst_th (_,subst,th) = 
@@ -255,17 +354,23 @@ let subst_th (_,subst,th) =
   let thm1' = subst_mps subst th.ring_lemma1 in
   let thm2' = subst_mps subst th.ring_lemma2 in
   let tac'= subst_tactic subst th.ring_cst_tac in
+  let pretac'= subst_tactic subst th.ring_pre_tac in
+  let posttac'= subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
      thm1' == th.ring_lemma1 &&
      thm2' == th.ring_lemma2 &&
-     tac' == th.ring_cst_tac then th
+     tac' == th.ring_cst_tac &&
+     pretac' == th.ring_pre_tac &&
+     posttac' == th.ring_post_tac then th
   else
     { ring_carrier = c';
       ring_req = eq';
       ring_cst_tac = tac';
       ring_lemma1 = thm1';
-      ring_lemma2 = thm2' }
+      ring_lemma2 = thm2';
+      ring_pre_tac = pretac';
+      ring_post_tac = posttac' }
 
 
 let (theory_to_obj, obj_to_theory) = 
@@ -280,10 +385,6 @@ let (theory_to_obj, obj_to_theory) =
       export_function = export_th }
 
 
-let ring_for_carrier r = Cmap.find r !from_carrier
-
-let ring_for_relation rel = Cmap.find rel !from_relation
-
 let setoid_of_relation r =
   lapp coq_mk_Setoid
     [|r.rel_a; r.rel_aeq;
@@ -293,14 +394,16 @@ let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
 
 let op_smorph r add mul req m1 m2 =
-  lapp coq_SReqe_Reqe
-    [| r;add;mul;req;lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]|]
+  lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
+
+let smorph2morph r add mul req sm =
+  lapp coq_SReqe_Reqe [| r;add;mul;req;sm|]
 
 let sr_sub r add = lapp coq_SRsub [|r;add|]
 let sr_opp r = lapp coq_SRopp [|r|]
 
-let dest_morphism kind th sth =
-  let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in
+let dest_morphism env sigma kind th sth =
+  let th_typ = Retyping.get_type_of env sigma th in
   match kind_of_term th_typ with
       App(f,[|_;_;_;_;_;_;_;_;c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
         when f = Lazy.force coq_ring_morph ->
@@ -311,16 +414,21 @@ let dest_morphism kind th sth =
           lapp coq_SRmorph_Rmorph
             [|r;zero;one;add;mul;req;sth;c;czero;cone;cadd;cmul;ceqb;phi;th|]in
         (th,[|c;czero;cone;cadd;cmul;cadd;sr_opp c;ceqb;phi|])
-    | _ -> failwith "bad ring_morph lemma"
+    | _ -> error "bad ring_morph lemma"
 
-let dest_eq_test th =
-  let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th in
+let dest_eq_test env sigma th =
+  let th_typ = Retyping.get_type_of env sigma th in
   match decompose_prod th_typ with
       (_,h)::_,_ ->
         (match snd(destApplication h) with
-            [|_;lhs;_|] -> fst(destApplication lhs)
-          | _ -> failwith "bad lemma for decidability of equality")
-    | _ -> failwith "bad lemma for decidability of equality"
+            [|_;lhs;_|] ->
+              let (f,args) = destApplication lhs in
+              if Array.length args < 2 then
+                error "bad lemma for decidability of equality"
+              else
+                mkApp(f,Array.sub args 0 (Array.length args -2))
+          | _ -> error "bad lemma for decidability of equality")
+    | _ -> error "bad lemma for decidability of equality"
 
 let default_ring_equality is_semi (r,add,mul,opp,req) =
   let is_setoid = function
@@ -348,7 +456,10 @@ let default_ring_equality is_semi (r,add,mul,opp,req) =
             error "ring multiplication should be declared as a morphism" in
         let op_morph =
           if is_semi <> Some true then
-            (let opp_m = default_morphism ~filter:is_endomorphism opp in
+            (let opp_m =
+              try default_morphism ~filter:is_endomorphism opp
+              with Not_found ->
+                error "ring opposite should be declared as a morphism" in
              let op_morph =
                op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in
              msgnl
@@ -372,8 +483,8 @@ let build_setoid_params is_semi r add mul opp req eqth =
       Some th -> th
     | None -> default_ring_equality is_semi (r,add,mul,opp,req)
 
-let dest_ring th_spec =
-  let th_typ = Retyping.get_type_of (Global.env()) Evd.empty th_spec in
+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 ->
@@ -403,42 +514,91 @@ type coeff_spec =
 
 type cst_tac_spec =
     CstTac of raw_tactic_expr
-  | Closed of constr list
-
-
-let add_theory name rth eqth morphth cst_tac =
-  Coqlib.check_required_library ["Coq";"setoid_ring";"Ring_tac"];
-  let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring rth in
+  | Closed of reference list
+
+(*
+let ring_equiv_constant c =
+  lazy (Coqlib.gen_constant_in_modules "Ring" [ring_dir@["Ring_equiv"]] c)
+let ring_def_eqb_ok = ring_equiv_constant "default_eqb_ok"
+let ring_equiv2 = ring_equiv_constant "ring_equiv2"
+let sring_equiv2 = ring_equiv_constant "sring_equiv2"
+let ring_m_plus = ring_constant "Radd_ext"
+let ring_m_mul = ring_constant "Rmul_ext"
+let ring_m_opp = ring_constant "Ropp_ext"
+
+let old_morph is_semi r add mul opp req morph =
+    { Ring.plusm = lapp ring_m_plus [|r;add;mul;opp;req;morph|];
+      Ring.multm  = lapp ring_m_mul [|r;add;mul;opp;req;morph|];
+      Ring.oppm =
+        if is_semi then None
+        else Some (lapp ring_m_opp [|r;add;mul;opp;req;morph|])
+    }
+
+let add_old_theory env sigma is_semi is_setoid
+      r zero one add mul sub opp req rth sth ops_morph morphth =
+(try
+  let opp_o = if is_semi then None else Some opp in
+  let (is_abs, eqb_ok) =
+    match morphth with
+        Computational c -> (false, c)
+      | _ -> (true, lapp ring_def_eqb_ok [|r|]) in
+  let eqb = dest_eq_test env sigma eqb_ok in
+  let rth =
+    if is_setoid then failwith "not impl"
+    else
+      if is_semi then
+        lapp sring_equiv2 [|r;zero;one;add;mul;rth;eqb;eqb_ok|]
+      else
+        lapp ring_equiv2 [|r;zero;one;add;mul;sub;opp;rth;eqb;eqb_ok|] in
+  Ring.add_theory (not is_semi) is_abs is_setoid r
+     (Some req) (Some sth)
+     (if is_setoid then Some(old_morph is_semi r add mul opp req ops_morph)
+      else None)
+     add mul one zero opp_o eqb rth Quote.ConstrSet.empty
+with _ ->
+  prerr_endline "Warning: could not add old ring structure")
+*)
+
+let add_theory name rth eqth morphth cst_tac (pre,post) =
+  let env = Global.env() in
+  let sigma = Evd.empty in
+  let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
   let (sth,morph) = build_setoid_params kind r add mul opp req eqth in
   let args0 = [|r;zero;one;add;mul;sub;opp;req;sth;morph|] in
+  let args0' = [|r;zero;one;add;mul;req;sth;morph|] in
   let (lemma1,lemma2) =
     match morphth with
       | Computational c ->
-          let reqb = dest_eq_test c in
+          let reqb = dest_eq_test env sigma c in
           let rth = 
             build_almost_ring
               kind r zero one add mul sub opp req sth  morph rth in
           let args = Array.append args0 [|rth;reqb;c|] in
           (lapp ring_comp1 args, lapp ring_comp2 args)
       | Morphism m ->
-          let (m,args1) = dest_morphism kind m sth in
+          let (m,args1) = dest_morphism env sigma kind m sth in
           let rth = 
             build_almost_ring
               kind r zero one add mul sub opp req sth morph rth in
           let args = Array.concat [args0;[|rth|]; args1; [|m|]] in
           (lapp coq_ring_lemma1 args, lapp coq_ring_lemma2 args)
       | Abstract ->
-          Coqlib.check_required_library ["Coq";"setoid_ring";"ZRing_th"];
-          let args1 = Array.append args0 [|rth|] in
+          (try check_required_library (ring_dir@["Ring"])
+          with UserError _ ->
+            error "You must require \"Ring\" to declare an abstract ring");
           (match kind with
               None -> error "an almost_ring cannot be abstract"
             | Some true ->
+                let args1 = Array.append args0' [|rth|] in
                 (lapp sring_abs1 args1, lapp sring_abs2 args1)
             | Some false ->
+                let args1 = Array.append args0 [|rth|] in
                 (lapp ring_abs1 args1, lapp ring_abs2 args1)) in
+  let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
+  let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
   let cst_tac = match cst_tac with
       Some (CstTac t) -> Tacinterp.glob_tactic t
-    | Some (Closed lc) -> failwith "TODO"
+    | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc)
     | None ->
         (match kind with
             Some true ->
@@ -448,6 +608,14 @@ let add_theory name rth eqth morphth cst_tac =
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | _ -> error"a tactic must be specified for an almost_ring") in
+  let pretac =
+    match pre with
+        Some t -> Tacinterp.glob_tactic t
+      | _ -> TacId [] in
+  let posttac =
+    match post with
+        Some t -> Tacinterp.glob_tactic t
+      | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
       (theory_to_obj
@@ -455,71 +623,499 @@ let add_theory name rth eqth morphth cst_tac =
           ring_req = req;
           ring_cst_tac = cst_tac;
           ring_lemma1 = lemma1;
-          ring_lemma2 = lemma2 }) in
+          ring_lemma2 = lemma2;
+          ring_pre_tac = pretac;
+          ring_post_tac = posttac }) in
+  (* old ring theory *)
+(*  let _ =
+    match kind with
+        Some is_semi ->
+          add_old_theory env sigma is_semi (eqth <> None)
+            r zero one add mul sub opp req rth sth morph morphth
+      | _ -> () in
+*)
   ()
 
-VERNAC ARGUMENT EXTEND ring_coefs
-| [ "Computational" constr(c)] -> [ Computational (ic c) ]
-| [ "Abstract" ] -> [ Abstract ]
-| [ "Coefficients" constr(m)] -> [ Morphism (ic m) ]
-| [ ] -> [ Abstract ]
+type ring_mod =
+    Ring_kind of coeff_spec
+  | Const_tac of cst_tac_spec
+  | Pre_tac of raw_tactic_expr
+  | Post_tac of raw_tactic_expr
+  | Setoid of Topconstr.constr_expr * Topconstr.constr_expr
+
+VERNAC ARGUMENT EXTEND ring_mod
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ]
+  | [ "abstract" ] -> [ Ring_kind Abstract ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic morph)) ]
+  | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
+  | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
+  | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
+  | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ]
+  | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ]
 END
 
-VERNAC ARGUMENT EXTEND ring_cst_tac
-| [ "Constant" tactic(c)] -> [ Some(CstTac c) ]
-| [ "[" ne_constr_list(l) "]" ] -> [ Some(Closed (List.map ic l)) ]
-| [ ] -> [ None ]
-END
+let set_once s r v =
+  if !r = None then r := Some v else error (s^" cannot be set twice")
+
+let process_ring_mods l =
+  let kind = ref None in
+  let set = ref None in
+  let cst_tac = ref None in
+  let pre = ref None in
+  let post = ref None in
+  List.iter(function
+      Ring_kind k -> set_once "ring kind" kind k
+    | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
+    | Pre_tac t -> set_once "preprocess tactic" pre t
+    | Post_tac t -> set_once "postprocess tactic" post t
+    | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)) l;
+  let k = match !kind with Some k -> k | None -> Abstract in
+  (k, !set, !cst_tac, !pre, !post)
 
 VERNAC COMMAND EXTEND AddSetoidRing
-| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c)
-      "Setoid" constr(e) constr(m) ring_cst_tac(tac) ] ->
-    [ add_theory id (ic t) (Some (ic e, ic m)) c tac ]
-| [ "Add" "New" "Ring" ident(id) ":" constr(t) ring_coefs(c) 
-      ring_cst_tac(tac) ] ->
-    [ add_theory id (ic t) None c tac ]
+  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
+    [ let (k,set,cst,pre,post) = process_ring_mods l in
+      add_theory id (ic t) set k cst (pre,post) ]
 END
 
-
 (*****************************************************************************)
 (* The tactics consist then only in a lookup in the ring database and
    call the appropriate ltac. *)
 
 let ring gl = 
-  let req = dest_rel (pf_concl gl) in
-  let e =
-    try ring_for_relation req
-    with Not_found ->
-      errorlabstrm "ring"
-        (str"cannot find a declared ring structure for equality"++
-         spc()++str"\""++pr_constr req++str"\"") in
-  Tacinterp.eval_tactic
-    (TacArg(TacCall(dummy_loc,
-      ArgArg(dummy_loc, Lazy.force ltac_setoid_ring),
-      Tacexp e.ring_cst_tac::
-      List.map carg [e.ring_lemma1;e.ring_lemma2;e.ring_req])))
-    gl
-
-let ring_rewrite rl =
-  let ty = Retyping.get_type_of (Global.env()) Evd.empty (List.hd rl) in
-  let e =
-    try ring_for_carrier ty
-    with Not_found ->
-      errorlabstrm "ring"
-        (str"cannot find a declared ring structure over"++
-         spc()++str"\""++pr_constr ty++str"\"") in
-  let rl = List.fold_right (fun x l -> lapp coq_cons [|ty;x;l|]) rl
-    (lapp coq_nil [|ty|]) in
+  let env = pf_env gl in
+  let sigma = project gl in
+  let e = find_ring_structure env sigma [] (pf_concl gl) None in
+  let main_tac =
+    ltac_call ltac_setoid_ring
+      (Tacexp e.ring_cst_tac:: List.map carg [e.ring_lemma1;e.ring_req]) in
+  Tacinterp.eval_tactic (TacThen(e.ring_pre_tac,main_tac)) gl
+
+let ring_rewrite rl gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let e = find_ring_structure env sigma rl (pf_concl gl) None in
+  let rl =
+    match rl with
+        [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2]
+      | _ -> rl in
+  let rl = List.fold_right
+    (fun x l -> lapp coq_cons [|e.ring_carrier;x;l|]) rl
+    (lapp coq_nil [|e.ring_carrier|]) in
+  let main_tac =
+    ltac_call ltac_setoid_ring_rewrite
+      (Tacexp e.ring_cst_tac::List.map carg [e.ring_lemma2;e.ring_req;rl]) in
   Tacinterp.eval_tactic
-    (TacArg(TacCall(dummy_loc,
-      ArgArg(dummy_loc, Lazy.force ltac_setoid_ring_rewrite),
-      Tacexp e.ring_cst_tac::List.map carg [e.ring_lemma2;e.ring_req;rl])))
-
-let setoid_ring = function
-  | [] -> ring
-  | l -> ring_rewrite l
+    (TacThen(e.ring_pre_tac,TacThen(main_tac,e.ring_post_tac))) gl
 
 TACTIC EXTEND setoid_ring
-  [ "setoid" "ring" constr_list(l) ] -> [ setoid_ring l ]
+  [ "ring" ] -> [ ring ]
+| [ "ring_simplify" constr_list(l) ] -> [ ring_rewrite l ]
+END
+
+(***********************************************************************)
+let fld_cst s = mk_cst [contrib_name;"NewField"] s ;;
+
+let field_modules = List.map
+  (fun f -> ["Coq";contrib_name;f])
+  ["NewField";"Field_tac"]
+
+let new_field_path =
+  make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"])
+
+let field_constant c =
+  lazy (Coqlib.gen_constant_in_modules "Field" field_modules c)
+
+let field_ltac s =
+  lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
+
+let field_lemma = field_constant "Fnorm_correct2"
+let field_simplify_eq_lemma = field_constant "Field_simplify_eq_correct"
+let field_simplify_lemma = field_constant "Pphi_dev_div_ok"
+
+let afield_theory = field_constant "almost_field_theory"
+let field_theory = field_constant "field_theory"
+let sfield_theory = field_constant "semi_field_theory"
+let field_Rth = field_constant "AF_AR"
+
+let field_tac = field_ltac "Make_field_tac"
+let field_simplify_eq_tac = field_ltac "Make_field_simplify_eq_tac"
+let field_simplify_tac = field_ltac "Make_field_simplify_tac"
+
+
+let _ = add_map "field"
+  (map_with_eq
+    [coq_cons,(function -1->Eval|2->Rec|_->Prot);
+    coq_nil, (function -1->Eval|_ -> Prot);
+    (* Pphi_dev: evaluate polynomial and coef operations, protect
+       ring operations and make recursive call on the var map *)
+    pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot);
+    (* PEeval: evaluate morphism and polynomial, protect ring 
+       operations and make recursive call on the var map *)
+    pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot);
+(*    fld_cst "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot);*)
+    (* PCond: evaluate morphism and denum list, protect ring
+       operations and make recursive call on the var map *)
+    fld_cst "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);;
+
+
+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 ->
+        let rth = lapp field_Rth
+          [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
+        (None,r,zero,one,add,mul,sub,opp,div,inv,req,rth)
+    | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
+        when f = Lazy.force field_theory ->
+        let rth =
+          lapp (field_constant"F_R")
+            [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
+        (Some false,r,zero,one,add,mul,sub,opp,div,inv,req,rth)
+    | App(f,[|r;zero;one;add;mul;div;inv;req|])
+        when f = Lazy.force sfield_theory ->
+        let rth = lapp (field_constant"SF_SR")
+          [|r;zero;one;add;mul;div;inv;req;th_spec|] in
+        (Some true,r,zero,one,add,mul,sr_sub r add,sr_opp r,div,inv,req,rth)
+    | _ -> error "bad field structure"
+
+let build_almost_field
+     kind r zero one add mul sub opp div inv req sth morph th =
+  match kind with
+      None -> th
+    | Some true ->
+        lapp (field_constant "SF2AF")
+          [|r;zero;one;add;mul;div;inv;req;sth;th|]
+    | Some false ->
+        lapp (field_constant "F2AF")
+          [|r;zero;one;add;mul;sub;opp;div;inv;req;sth;morph;th|]
+
+type field_info =
+    { field_carrier : types;
+      field_req : constr;
+      field_cst_tac : glob_tactic_expr;
+      field_ok : constr;
+      field_simpl_eq_ok : constr;
+      field_simpl_ok : constr;
+      field_cond : constr;
+      field_pre_tac : glob_tactic_expr;
+      field_post_tac : glob_tactic_expr }
+
+let field_from_carrier = ref Cmap.empty
+let field_from_relation = ref Cmap.empty
+let field_from_name = ref Spmap.empty
+
+
+let field_for_carrier r = Cmap.find r !field_from_carrier
+let field_for_relation rel = Cmap.find rel !field_from_relation
+let field_lookup_by_name ref =
+  Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref)))
+    !field_from_name
+
+
+let find_field_structure env sigma l cl oname =
+  check_required_library (ring_dir@["Field_tac"]);
+  match oname, l with
+      Some rf, _ ->
+        (try field_lookup_by_name rf
+        with Not_found ->
+          errorlabstrm "field"
+            (str "found no field named "++pr_reference rf))
+    | None, t::cl' ->
+        let ty = Retyping.get_type_of env sigma t in
+        let check c =
+          let ty' = Retyping.get_type_of env sigma c in
+          if not (Reductionops.is_conv env sigma ty ty') then
+            errorlabstrm "field"
+              (str"arguments of field_simplify do not have all the same type")
+        in
+        List.iter check cl';
+        (try field_for_carrier ty
+        with Not_found ->
+          errorlabstrm "field"
+            (str"cannot find a declared field structure over"++
+             spc()++str"\""++pr_constr ty++str"\""))
+    | None, [] ->
+        let (req,_,_) = dest_rel cl in
+        (try field_for_relation req
+        with Not_found ->
+          errorlabstrm "field"
+            (str"cannot find a declared field structure for equality"++
+             spc()++str"\""++pr_constr req++str"\""))
+
+let _ = 
+  Summary.declare_summary "tactic-new-field-table"
+    { Summary.freeze_function =
+        (fun () -> !field_from_carrier,!field_from_relation,!field_from_name);
+      Summary.unfreeze_function =
+        (fun (ct,rt,nt) ->
+          field_from_carrier := ct; field_from_relation := rt;
+          field_from_name := nt);
+      Summary.init_function =
+        (fun () ->
+          field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty;
+          field_from_name := Spmap.empty);
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+let add_field_entry (sp,_kn) e =
+  let _ = ty e.field_ok in
+  let _ = ty e.field_simpl_eq_ok in
+  let _ = ty e.field_simpl_ok in
+  let _ = ty e.field_cond in
+  field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier;
+  field_from_relation := Cmap.add e.field_req e !field_from_relation;
+  field_from_name := Spmap.add sp e !field_from_name 
+
+
+let subst_th (_,subst,th) = 
+  let c' = subst_mps subst th.field_carrier in                   
+  let eq' = subst_mps subst th.field_req in
+  let thm1' = subst_mps subst th.field_ok in
+  let thm2' = subst_mps subst th.field_simpl_eq_ok in
+  let thm3' = subst_mps subst th.field_simpl_ok in
+  let thm4' = subst_mps subst th.field_cond in
+  let tac'= subst_tactic subst th.field_cst_tac in
+  let pretac'= subst_tactic subst th.field_pre_tac in
+  let posttac'= subst_tactic subst th.field_post_tac in
+  if c' == th.field_carrier &&
+     eq' == th.field_req &&
+     thm1' == th.field_ok &&
+     thm2' == th.field_simpl_eq_ok &&
+     thm3' == th.field_simpl_ok &&
+     thm4' == th.field_cond &&
+     tac' == th.field_cst_tac &&
+     pretac' == th.field_pre_tac &&
+     posttac' == th.field_post_tac then th
+  else
+    { field_carrier = c';
+      field_req = eq';
+      field_cst_tac = tac';
+      field_ok = thm1';
+      field_simpl_eq_ok = thm2';
+      field_simpl_ok = thm3';
+      field_cond = thm4';
+      field_pre_tac = pretac';
+      field_post_tac = posttac' }
+
+
+let (ftheory_to_obj, obj_to_ftheory) = 
+  let cache_th (name,th) = add_field_entry name th
+  and export_th x = Some x in
+  declare_object
+    {(default_object "tactic-new-field-theory") with
+      open_function = (fun i o -> if i=1 then cache_th o);
+      cache_function = cache_th;
+      subst_function = subst_th;
+      classify_function = (fun (_,x) -> Substitute x);
+      export_function = export_th }
+
+let default_field_equality r inv req =
+  let is_setoid = function
+      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
+    | _ -> false in
+  match default_relation_for_carrier ~filter:is_setoid r with
+      Leibniz _ ->
+        mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
+    | Relation rel ->
+        let is_endomorphism = function
+            { args=args } -> List.for_all
+                (function (var,Relation rel) ->
+                  var=None && eq_constr req rel
+                  | _ -> false) args in
+        let inv_m =
+          try default_morphism ~filter:is_endomorphism inv
+          with Not_found ->
+            error "field inverse should be declared as a morphism" in
+        inv_m.lem
+
+
+let n_morph r zero one add mul =
+[|Lazy.force(coq_constant"N");
+Lazy.force(coq_constant"N0");
+lapp(coq_constant"Npos")[|Lazy.force(coq_constant"xH")|];
+Lazy.force(coq_constant"Nplus");
+Lazy.force(coq_constant"Nmult");
+Lazy.force(coq_constant"Nminus");
+Lazy.force(coq_constant"Nopp");
+Lazy.force(ring_constant"Neq_bool");
+lapp(ring_constant"gen_phiN")[|r;zero;one;add;mul|]
+|]
+let z_morph r zero one add mul opp =
+[|Lazy.force(coq_constant"Z");
+Lazy.force(coq_constant"Z0");
+lapp(coq_constant"Zpos")[|Lazy.force(coq_constant"xH")|];
+Lazy.force(coq_constant"Zplus");
+Lazy.force(coq_constant"Zmult");
+Lazy.force(coq_constant"Zminus");
+Lazy.force(coq_constant"Zopp");
+Lazy.force(coq_constant"Zeq_bool");
+lapp(ring_constant"gen_phiZ")[|r;zero;one;add;mul;opp|]
+|]
+
+let add_field_theory name fth eqth morphth cst_tac inj (pre,post) =
+  let env = Global.env() in
+  let sigma = Evd.empty in
+  let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
+    dest_field env sigma fth in
+  let (sth,morph) = build_setoid_params None r add mul opp req eqth in
+  let eqth = Some(sth,morph) in
+  let _ = add_theory name rth eqth morphth cst_tac (None,None) in
+  let afth = build_almost_field
+    kind r zero one add mul sub opp div inv req sth morph fth in
+  let inv_m = default_field_equality r inv req in
+  let args0 =
+    [|r;zero;one;add;mul;sub;opp;div;inv;req;sth;morph;inv_m;afth|] in
+  let args0' =
+    [|r;zero;one;add;mul;sub;opp;div;inv;req;sth;morph;afth|] in
+  let (m,args1) =
+    match morphth with
+        Computational c ->
+          let reqb = dest_eq_test env sigma c in
+          let idphi = ring_constant "IDphi" in
+          let idmorph =  lapp (ring_constant "IDmorph")
+            [|r;zero;one;add;mul;sub;opp;req;sth;reqb;c|] in
+          (idmorph,[|r;zero;one;add;mul;sub;opp;reqb;lapp idphi [|r|]|])
+      | Morphism m ->
+          dest_morphism env sigma kind m sth
+      | Abstract ->
+          (match kind with
+              None -> error "an almost_field cannot be abstract"
+            | Some true ->
+                (lapp(ring_constant"gen_phiN_morph")
+                  [|r;zero;one;add;mul;req;sth;morph;rth|],
+                 n_morph r zero one add mul)
+            | Some false ->
+                (lapp(ring_constant"gen_phiZ_morph")
+                  [|r;zero;one;add;mul;sub;opp;req;sth;morph;rth|],
+                 z_morph r zero one add mul opp)) in
+  let args = Array.concat [args0;args1;[|m|]] in
+  let args' = Array.concat [args0';args1;[|m|]] in
+  let lemma1 = lapp field_lemma args in
+  let lemma2 = lapp field_simplify_eq_lemma args in
+  let lemma3 = lapp field_simplify_lemma args in
+  let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in
+  let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in
+  let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
+  let cond_lemma =
+    match inj with
+      | Some thm ->
+          lapp (field_constant"Pcond_simpl_complete")
+            (Array.append args' [|thm|])
+      | None -> lapp (field_constant"Pcond_simpl_gen") args' in
+  let cond_lemma = decl_constant (string_of_id name^"_lemma4") cond_lemma in
+  let cst_tac = match cst_tac with
+      Some (CstTac t) -> Tacinterp.glob_tactic t
+    | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc)
+    | None ->
+        (match kind with
+            Some true ->
+              let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
+              TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
+          | Some false ->
+              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
+              TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+          | _ -> error"a tactic must be specified for an almost_ring") in
+  let pretac =
+    match pre with
+        Some t -> Tacinterp.glob_tactic t
+      | _ -> TacId [] in
+  let posttac =
+    match post with
+        Some t -> Tacinterp.glob_tactic t
+      | _ -> TacId [] in
+  let _ =
+    Lib.add_leaf name
+      (ftheory_to_obj
+        { field_carrier = r;
+          field_req = req;
+          field_cst_tac = cst_tac;
+          field_ok = lemma1;
+          field_simpl_eq_ok = lemma2;
+          field_simpl_ok = lemma3;
+          field_cond = cond_lemma;
+          field_pre_tac = pretac;
+          field_post_tac = posttac }) in  ()
+
+type field_mod =
+    Ring_mod of ring_mod
+  | Inject of Topconstr.constr_expr
+
+VERNAC ARGUMENT EXTEND field_mod
+  | [ ring_mod(m) ] -> [ Ring_mod m ]
+  | [ "infinite" constr(inj) ] -> [ Inject inj ]
+END
+
+let process_field_mods l =
+  let kind = ref None in
+  let set = ref None in
+  let cst_tac = ref None in
+  let pre = ref None in
+  let post = ref None in
+  let inj = ref None in
+  List.iter(function
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind k
+    | Ring_mod(Const_tac t) ->
+        set_once "tactic recognizing constants" cst_tac t
+    | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
+    | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
+    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext)
+    | Inject i -> set_once "infinite property" inj (ic i)) l;
+  let k = match !kind with Some k -> k | None -> Abstract in
+  (k, !set, !inj, !cst_tac, !pre, !post)
+
+VERNAC COMMAND EXTEND AddSetoidField
+| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> 
+  [ let (k,set,inj,cst_tac,pre,post) = process_field_mods l in
+    add_field_theory id (ic t) set k cst_tac inj (pre,post) ]
 END
 
+let field gl = 
+  let env = pf_env gl in
+  let sigma = project gl in
+  let e = find_field_structure env sigma [] (pf_concl gl) None in
+  let main_tac =
+    ltac_call field_tac
+      [carg e.field_ok;carg e.field_cond;
+       carg e.field_req; Tacexp e.field_cst_tac] in
+  Tacinterp.eval_tactic
+    (TacThen(e.field_pre_tac,TacThen(main_tac,e.field_post_tac))) gl
+
+let field_simplify_eq gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let e = find_field_structure env sigma [] (pf_concl gl) None in
+  let main_tac =
+    ltac_call field_simplify_eq_tac
+      [carg e.field_simpl_eq_ok;carg e.field_cond;
+       carg e.field_req; Tacexp e.field_cst_tac] in
+  Tacinterp.eval_tactic
+    (TacThen(e.field_pre_tac,TacThen(main_tac,e.field_post_tac))) gl
+
+let field_simplify rl gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let e = find_field_structure env sigma rl (pf_concl gl) None in
+  let rl =
+    match rl with
+        [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2]
+      | _ -> rl in
+  let rl = List.fold_right
+    (fun x l -> lapp coq_cons [|e.field_carrier;x;l|]) rl
+    (lapp coq_nil [|e.field_carrier|]) in
+  let main_tac =
+    ltac_call field_simplify_tac
+      [carg e.field_simpl_ok;carg e.field_cond;
+       carg e.field_req; Tacexp e.field_cst_tac;
+       carg rl] in
+  Tacinterp.eval_tactic
+    (TacThen(e.field_pre_tac,TacThen(main_tac,e.field_post_tac))) gl
+
+TACTIC EXTEND setoid_field
+  [ "field" ] -> [ field ]
+END
+TACTIC EXTEND setoid_field_simplify
+  [ "field_simplify_eq" ] -> [ field_simplify_eq ]
+| [ "field_simplify" constr_list(l) ] -> [ field_simplify l ]
+END