26 files changed, 499 insertions, 547 deletions

diff --git a/.depend.coq b/.depend.coq
index 2ea701f0a..16ee9a7d1 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -28,9 +28,10 @@ theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface
 theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo
 theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo
-theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo contrib/field/LegacyField.vo
+theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
+theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo
 theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
 theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
@@ -121,11 +122,11 @@ theories/Logic/ClassicalEpsilon.vo: theories/Logic/ClassicalEpsilon.v theories/L
 theories/Logic/ClassicalUniqueChoice.vo: theories/Logic/ClassicalUniqueChoice.v theories/Logic/Classical.vo theories/Setoids/Setoid.vo
 theories/Logic/DecidableType.vo: theories/Logic/DecidableType.v theories/Lists/SetoidList.vo
 theories/Logic/DecidableTypeEx.vo: theories/Logic/DecidableTypeEx.v theories/Logic/DecidableType.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo
-theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo contrib/setoid_ring/ArithRing.vo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Arith_base.vo contrib/setoid_ring/ArithRing.vo
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Le.vo: theories/Arith/Le.v
-theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith_base.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
 theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Logic/Decidable.vo
 theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Le.vo
@@ -141,6 +142,7 @@ theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
 theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Bool/Sumbool.vo
 theories/Arith/Factorial.vo: theories/Arith/Factorial.v theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Lt.vo
+theories/Arith/Arith_base.vo: theories/Arith/Arith_base.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo
 theories/Bool/Bool.vo: theories/Bool/Bool.v
 theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
@@ -160,14 +162,14 @@ theories/ZArith/BinInt.vo: theories/ZArith/BinInt.v theories/NArith/BinPos.vo th
 theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Znat.vo theories/ZArith/Zmisc.vo theories/Arith/Wf_nat.vo
 theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zpower.vo theories/ZArith/Zdiv.vo theories/ZArith/Zlogarithm.vo
 theories/ZArith/ZArith_dec.vo: theories/ZArith/ZArith_dec.v theories/Bool/Sumbool.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo
-theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/ZArith/auxiliary.vo: theories/ZArith/auxiliary.v theories/Arith/Arith_base.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
 theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/Bool/Bool.vo
 theories/ZArith/Zcompare.vo: theories/ZArith/Zcompare.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo
-theories/ZArith/Znat.vo: theories/ZArith/Znat.v theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
-theories/ZArith/Zorder.vo: theories/ZArith/Zorder.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/Arith/Arith.vo theories/Logic/Decidable.vo theories/ZArith/Zcompare.vo
-theories/ZArith/Zabs.vo: theories/ZArith/Zabs.v theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/ZArith_dec.vo
-theories/ZArith/Zmin.vo: theories/ZArith/Zmin.v theories/Arith/Arith.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo
-theories/ZArith/Zmax.vo: theories/ZArith/Zmax.v theories/Arith/Arith.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo
+theories/ZArith/Znat.vo: theories/ZArith/Znat.v theories/Arith/Arith_base.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/ZArith/Zorder.vo: theories/ZArith/Zorder.v theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/Arith/Arith_base.vo theories/Logic/Decidable.vo theories/ZArith/Zcompare.vo
+theories/ZArith/Zabs.vo: theories/ZArith/Zabs.v theories/Arith/Arith_base.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/ZArith_dec.vo
+theories/ZArith/Zmin.vo: theories/ZArith/Zmin.v theories/Arith/Arith_base.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo
+theories/ZArith/Zmax.vo: theories/ZArith/Zmax.v theories/Arith/Arith_base.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo
 theories/ZArith/Zminmax.vo: theories/ZArith/Zminmax.v theories/ZArith/Zmin.vo theories/ZArith/Zmax.vo theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo
 theories/ZArith/Zeven.vo: theories/ZArith/Zeven.v theories/ZArith/BinInt.vo
 theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo
@@ -272,9 +274,10 @@ theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theo
 theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rdefinitions.vo
-theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo contrib/field/LegacyField.vo
+theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/RealField.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
+theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo
 theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
 theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
@@ -364,11 +367,11 @@ contrib/setoid_ring/BinList.vo: contrib/setoid_ring/BinList.v theories/NArith/Bi
 contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo
 contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/newring.cmo
-contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo
-contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring_polynom.vo
+contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/InitialRing.vo
+contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/Ring_polynom.vo
 contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo
-contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo
-contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo contrib/setoid_ring/Ring_base.vo
+contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring_tac.vo
+contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo
 contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo
 contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
 contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
diff --git a/Makefile b/Makefile
index 25dd5e2ed..f4de7a9ca 100644
--- a/Makefile
+++ b/Makefile
@@ -842,7 +842,7 @@ ARITHVO=\
  theories/Arith/Euclid.vo       theories/Arith/Plus.vo        \
  theories/Arith/Wf_nat.vo  	theories/Arith/Max.vo	      \
  theories/Arith/Bool_nat.vo	theories/Arith/Factorial.vo   \
-# theories/Arith/Div.vo 
+ theories/Arith/Arith_base.vo 
 
 SORTINGVO=\
  theories/Sorting/Heap.vo	theories/Sorting/Permutation.vo \
@@ -960,6 +960,7 @@ REALSBASEVO=\
  theories/Reals/Rdefinitions.vo \
  theories/Reals/Raxioms.vo      theories/Reals/RIneq.vo \
  theories/Reals/DiscrR.vo       theories/Reals/Rbase.vo \
+ theories/Reals/LegacyRfield.vo
 
 REALS_basic= 
 
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 0f99432dc..ac65f826e 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -9,6 +9,8 @@
 Require Import Mult.
 Require Import Ring_base.
 Set Implicit Arguments.
+Require Import InitialRing.
+Export Ring_tac.
 
 Ltac isnatcst t :=
   let t := eval hnf in t in
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index c7d3ff8f9..91ccf2216 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -82,7 +82,7 @@ Ltac simpl_PCond req :=
   fold_field_cond req.
 
 (* Rewriting (field_simplify) *)
-Ltac Make_field_simplify_tac lemma Cond_lemma req Cst_tac :=
+Ltac Field_simplify lemma Cond_lemma req Cst_tac :=
   let Make_tac :=
     match type of lemma with
     | forall l fe nfe,
@@ -100,6 +100,10 @@ Ltac Make_field_simplify_tac lemma Cond_lemma req Cst_tac :=
   Make_tac ReflexiveRewriteTactic.
 (* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
 
+Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
+  field_lookup (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl =>
+    (pre(); Field_simplify field_simplify_ok cond_ok req cst_tac; post())).
+
 
 (* Generic form of field tactics *)
 Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
@@ -158,41 +162,69 @@ Ltac Field_Scheme_n FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
            ((apply ilemma || fail "field anomaly: failed in applying lemma");
            [ SIMPL_tac | apply Cond_lemma; simpl_PCond req])) in
   OnEquation req Main.
-(*
-Ltac ParseFieldComponents lemma req :=
-  match type of lemma with
-  | forall l fe1 fe2 nfe1 nfe2,
-    _ = nfe1 -> _ = nfe2 -> _ -> PCond _ _ _ _ _ _ _ _ _ ->
-    req (@FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi l fe1) _ =>
-      (fun f => f add mul sub opp div inv C)
-  | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
-  end.
-*)
+
 (* solve completely a field equation, leaving non-zero conditions to be
    proved (field) *)
-Ltac Make_field_tac lemma Cond_lemma req Cst_tac :=
+Ltac Field lemma Cond_lemma req Cst_tac :=
   let Main radd rmul rsub ropp rdiv rinv C :=
     let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
     let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
     let Simpl :=
       vm_compute; (reflexivity || fail "not a valid field equation") in
-    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
+    Field_Scheme_n mkFV mkFE Simpl lemma Cond_lemma req in
   ParseFieldComponents lemma req Main.
 
+Tactic Notation (at level 0) "field" :=
+  field_lookup (fun req cst_tac field_ok _ _ cond_ok pre post rl =>
+    (pre(); Field field_ok cond_ok req cst_tac; post())).
+
 (* transforms a field equation to an equivalent (simplified) ring equation,
    and leaves non-zero conditions to be proved (field_simplify_eq) *)
-Ltac Make_field_simplify_eq_old_tac lemma Cond_lemma req Cst_tac :=
-  let Main radd rmul rsub ropp rdiv rinv C :=
-    let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
-    let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
-    let Simpl := (protect_fv "field") in
-    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
-  ParseFieldComponents lemma req Main.
-
-Ltac Make_field_simplify_eq_tac lemma Cond_lemma req Cst_tac :=
+Ltac Field_simplify_eq lemma Cond_lemma req Cst_tac :=
   let Main radd rmul rsub ropp rdiv rinv C :=
     let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
     let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
     let Simpl := (protect_fv "field") in
     Field_Scheme_n mkFV mkFE Simpl lemma Cond_lemma req in
   ParseFieldComponents lemma req Main.
+
+Tactic Notation (at level 0) "field_simplify_eq" constr_list(rl) :=
+  field_lookup (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl =>
+    (pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac;
+     post())) rl.
+
+(* Adding a new field *)
+
+Ltac ring_of_field f :=
+  match type of f with
+  | almost_field_theory _ _ _ _ _ _ _ _ _ => constr:(AF_AR f)
+  | field_theory _ _ _ _ _ _ _ _ _ => constr:(F_R f)
+  | semi_field_theory _ _ _ _ _ _ _ => constr:(SF_SR f)
+  end.
+
+Ltac coerce_to_almost_field set ext f :=
+  match type of f with
+  | almost_field_theory _ _ _ _ _ _ _ _ _ => f
+  | field_theory _ _ _ _ _ _ _ _ _ => constr:(F2AF set ext f)
+  | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f)
+  end.
+
+Ltac field_elements set ext fspec rk :=
+  let afth := coerce_to_almost_field set ext fspec in
+  let rspec := ring_of_field fspec in
+  ring_elements set ext rspec rk
+  ltac:(fun arth ext_r morph f => f afth ext_r morph).
+
+
+Ltac field_lemmas set ext inv_m fspec rk :=
+  field_elements set ext fspec rk
+  ltac:(fun afth ext_r morph =>
+    let field_ok := constr:(Field_correct set ext_r inv_m afth morph) in
+    let field_simpl_ok :=
+      constr:(Pphi_dev_div_ok set ext_r inv_m afth morph) in
+    let field_simpl_eq_ok :=
+      constr:(Field_simplify_eq_correct set ext_r inv_m afth morph) in
+    let cond1_ok := constr:(Pcond_simpl_gen set ext_r afth morph) in
+    let cond2_ok := constr:(Pcond_simpl_complete set ext_r afth morph) in
+    (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok
+                cond1_ok cond2_ok)).
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 17d05c9c3..f810859c3 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Ring.
-Import Ring_polynom Ring_theory InitialRing Setoid List.
+Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List.
 Require Import ZArith_base.
 Set Implicit Arguments.
 
@@ -982,16 +982,16 @@ Proof.
 Qed.
 
 (* solving a field equation *)
-Theorem Fnorm_correct2:
- forall l fe1 fe2 nfe1 nfe2,
- Fnorm fe1 = nfe1 ->
- Fnorm fe2 = nfe2 ->
+Theorem Field_correct :
+ forall l fe1 fe2,
+ forall nfe1, Fnorm fe1 = nfe1 ->
+ forall nfe2, Fnorm fe2 = nfe2 ->
  Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2)))
           (Nnorm (PEmul (num nfe2) (denum nfe1))) = true ->
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 Proof.
-intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hnorm Hcond; subst nfe1 nfe2.
+intros l fe1 fe2 nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2.
 apply Fnorm_crossproduct; trivial.
 apply (ring_correct Rsth Reqe ARth CRmorph); trivial.
 Qed.
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 44f2f9501..7df68cc05 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -10,7 +10,8 @@ Require Import ZArith_base.
 Require Import BinInt.
 Require Import BinNat.
 Require Import Setoid.
-Require Import Ring_base.
+Require Import Ring_theory.
+Require Import Ring_tac.
 Require Import Ring_polynom.
 Set Implicit Arguments.
 
@@ -404,7 +405,7 @@ Definition ring_gen_correct
                 (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).
+                (gen_phiZ_morph rSet req_th Rth).
 
 Definition ring_rw_gen_correct
   R rO rI radd rmul rsub ropp req rSet req_th Rth :=
@@ -412,7 +413,7 @@ Definition ring_rw_gen_correct
                  (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).
+                 (gen_phiZ_morph rSet req_th Rth).
 
 Definition ring_gen_eq_correct R rO rI radd rmul rsub ropp Rth :=
   @ring_gen_correct
@@ -434,7 +435,7 @@ Definition ring_gen_correct
                 (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).
+                (gen_phiN_morph rSet req_th SRth).
 
 Definition ring_rw_gen_correct
   R rO rI radd rmul req rSet req_th SRth :=
@@ -443,7 +444,7 @@ Definition ring_rw_gen_correct
                  (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).
+                 (gen_phiN_morph rSet req_th SRth).
 
 Definition ring_gen_eq_correct R rO rI radd rmul SRth :=
   @ring_gen_correct
@@ -454,3 +455,57 @@ Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth :=
      R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth.
 
 End Npol.
+
+
+Ltac coerce_to_almost_ring set ext rspec :=
+  match type of rspec with
+  | ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec)
+  | semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec)
+  | almost_ring_theory _ _ _ _ _ _ _ => rspec
+  | _ => fail 1 "not a valid ring theory"
+  end.
+
+Ltac coerce_to_ring_ext ext :=
+  match type of ext with
+  | ring_eq_ext _ _ _ _ => ext
+  | sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext)
+  | _ => fail 1 "not a valid ring_eq_ext theory"
+  end.
+
+Ltac abstract_ring_morphism set ext rspec :=
+  match type of rspec with
+  | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
+  | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
+  | almost_ring_theory _ _ _ _ _ _ _ =>
+      fail 1 "an almost ring cannot be abstract"
+  | _ => fail 1 "bad ring structure"
+  end.
+
+Ltac ring_elements set ext rspec rk :=
+  let arth := coerce_to_almost_ring set ext rspec in
+  let ext_r := coerce_to_ring_ext ext in
+  let morph :=
+    match rk with
+    | Abstract => abstract_ring_morphism set ext rspec
+    | @Computational ?reqb_ok =>
+        match type of arth with
+        | almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ =>
+            constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
+        | _ => fail 2 "ring anomaly"
+        end
+    | @Morphism ?m => m
+    | _ => fail 1 "ill-formed ring kind"
+    end in
+  fun f => f arth ext_r morph.
+
+(* Given a ring structure and the kind of morphism,
+   returns 2 lemmas (one for ring, and one for ring_simplify). *)
+
+Ltac ring_lemmas set ext rspec rk :=
+  ring_elements set ext rspec rk
+    ltac:(fun arth ext_r morph =>
+      let lemma1 := constr:(ring_correct set ext_r arth morph) in
+      let lemma2 := constr:(Pphi_dev_ok set ext_r arth morph) in
+      fun f => f arth ext_r morph lemma1 lemma2).
+
+
diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index 194c396ea..13896123b 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -1,6 +1,6 @@
 Require Import Raxioms.
 Require Import Rdefinitions.
-Require Import Ring Field.
+Require Export Ring Field.
 
 Open Local Scope R_scope.
 
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index cda2e0e50..167e026f6 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -9,7 +9,7 @@
 Require Import Bool.
 Require Export Ring_theory.
 Require Export Ring_base.
-Require Import InitialRing.
+Require Export Ring_tac.
 
 Lemma BoolTheory :
   ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
index e0ff5b023..95b037e3b 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/contrib/setoid_ring/Ring_base.v
@@ -13,3 +13,4 @@
 Declare ML Module "newring".
 Require Export Ring_theory.
 Require Export Ring_tac.
+Require Import InitialRing.
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index a6460ed5c..ec09d4f0b 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -5,6 +5,7 @@ Require Import Ring_polynom.
 Require Import BinList.
 Declare ML Module "newring".
 
+
 (* 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 :=
@@ -144,30 +145,16 @@ Ltac Ring_simplify Cst_tac lemma2 req rl :=
     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
-  R rO rI radd rmul rsub ropp req rSet req_th ARth reqb reqb_ok :=
-  @ring_correct 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
-                 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_id_eq_correct R rO rI radd rmul rsub ropp ARth reqb reqb_ok :=
- @ring_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.
+Tactic Notation (at level 0) "ring" :=
+  ring_lookup
+    (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
+       (pre(); Ring cst_tac lemma1 req)).
 
+Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
+  ring_lookup
+    (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
+       (pre(); Ring_simplify cst_tac lemma2 req rl; post())) rl.
+
+(* A simple macro tactic to be prefered to ring_simplify *)
+Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index dd83b05a8..2f7378eb0 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -433,8 +433,37 @@ Qed.
   repeat rewrite ARmul_0_r; sreflexivity.
  Qed.
 
+
+
 End ALMOST_RING.
 
+Section AddRing.
+
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable req : R -> R -> Prop.
+
+Inductive ring_kind : Type :=
+| Abstract
+| Computational
+    (R:Type)
+    (req : R -> R -> Prop)
+    (reqb : R -> R -> bool)
+    (_ : forall x y, (reqb x y) = true -> req x y)
+| Morphism
+    (R : Type)
+    (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R)
+    (req : R -> R -> Prop)
+    (C : Type)
+    (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C)
+    (ceqb : C->C->bool)
+    phi
+    (_ : ring_morph rO rI radd rmul rsub ropp req
+                    cO cI cadd cmul csub copp ceqb phi).
+
+End AddRing.
+
+
 (** Some simplification tactics*)
 Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth).
 
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4dbc725b8..5220c3a9c 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -9,6 +9,8 @@
 Require Export Ring.
 Require Import ZArith_base.
 Import InitialRing.
+Export Ring_tac.
+
 Set Implicit Arguments.
 
 Ltac isZcst t :=
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 046843866..fd5411a2f 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -145,28 +145,93 @@ let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
 *)
 
 (****************************************************************************)
-(* Library linking *)
 
-let contrib_name = "setoid_ring"
+let ic c =
+  let env = Global.env() and sigma = Evd.empty in
+  Constrintern.interp_constr sigma env c
 
+let ty c = Typing.type_of (Global.env()) Evd.empty c
+
+let decl_constant na c =
+  mkConst(declare_constant (id_of_string na) (DefinitionEntry 
+    { const_entry_body = c;
+      const_entry_type = None;
+      const_entry_opaque = true;
+      const_entry_boxed = true}, 
+    IsProof Lemma))
+
+let ltac_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+
+let ltac_lcall tac args =
+  TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+
+let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
+
+let dummy_goal env =
+  {Evd.it=
+    {Evd.evar_concl=mkProp;
+     Evd.evar_hyps=named_context_val env;
+     Evd.evar_body=Evd.Evar_empty;
+     Evd.evar_extra=None};
+   Evd.sigma=Evd.empty}
+
+let exec_tactic env n f args =
+  let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
+  let res = ref [||] in
+  let get_res ist =
+    let l = List.map (fun id ->  List.assoc id ist.lfun) lid in
+    res := Array.of_list l;
+    TacId[] in
+  let getter =
+    Tacexp(TacFun(List.map(fun id -> Some id) lid,
+                  glob_tactic(tacticIn get_res))) in
+  let _ =
+    Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
+  !res
+
+let constr_of = function
+  | VConstr c -> c
+  | _ -> failwith "Ring.exec_tactic: anomaly"
 
-let ring_dir = ["Coq";contrib_name]
-let ring_modules = 
-  [ring_dir@["BinList"];ring_dir@["Ring_theory"];ring_dir@["Ring_polynom"];
-   ring_dir@["Ring_tac"];ring_dir@["Field_tac"];ring_dir@["InitialRing"]]
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
-   ["Coq";"ZArith";"BinInt"];
-   ["Coq";"ZArith";"Zbool"];
-   ["Coq";"NArith";"BinNat"];
-   ["Coq";"NArith";"BinPos"]]
+   ["Coq";"Lists";"List"]
+  ]
 
 let coq_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
-let ring_constant c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" ring_modules c)
-let ringtac_constant m c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" [ring_dir@["InitialRing";m]] c)
+
+let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
+let coq_cons = coq_constant "cons"
+let coq_nil = coq_constant "nil"
+
+let lapp f args = mkApp(Lazy.force f,args)
+
+let rec dest_rel t =
+  match kind_of_term t with
+      App(f,args) when Array.length args >= 2 ->
+        let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
+        if closed0 rel then
+          (rel,args.(Array.length args - 2),args.(Array.length args - 1))
+        else error "ring: cannot find relation (not closed)"
+    | Prod(_,_,c) -> dest_rel c
+    | _ -> error "ring: cannot find relation"
+
+(****************************************************************************)
+(* Library linking *)
+
+let contrib_name = "setoid_ring"
+
+let cdir = ["Coq";contrib_name]
+let contrib_modules =
+  List.map (fun d -> cdir@d)
+    [["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"];
+     ["Field_tac"]; ["Field_theory"]
+    ]
+
+let my_constant c =
+  lazy (Coqlib.gen_constant_in_modules "Ring" contrib_modules c)
 
 let new_ring_path =
   make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"])
@@ -176,7 +241,6 @@ let znew_ring_path =
   make_dirpath (List.map id_of_string ["InitialRing";contrib_name;"Coq"])
 let zltac s =
   lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
-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;"Ring_polynom"] s ;;
@@ -184,59 +248,27 @@ let pol_cst s = mk_cst [contrib_name;"Ring_polynom"] s ;;
 (* 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 ring_comp1 = ring_constant "ring_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 sring_abs1 = ringtac_constant "Npol" "ring_gen_correct"
-let sring_abs2 = ringtac_constant "Npol" "ring_rw_gen_correct"
+let coq_almost_ring_theory = my_constant "almost_ring_theory"
 
 (* setoid and morphism utilities *)
-let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
-let coq_eq_setoid = ring_constant "Eqsth"
-let coq_eq_morph = ring_constant "Eq_ext"
+let coq_eq_setoid = my_constant "Eqsth"
+let coq_eq_morph = my_constant "Eq_ext"
+let coq_eq_smorph = my_constant "Eq_s_ext"
 
 (* ring -> almost_ring utilities *)
-let coq_ring_theory = ring_constant "ring_theory"
-let coq_ring_morph = ring_constant "ring_morph"
-let coq_Rth_ARth = ring_constant "Rth_ARth"
-let coq_mk_reqe = ring_constant "mk_reqe"
+let coq_ring_theory = my_constant "ring_theory"
+let coq_mk_reqe = my_constant "mk_reqe"
 
 (* semi_ring -> almost_ring utilities *)
-let coq_semi_ring_theory = ring_constant "semi_ring_theory"
-let coq_SRth_ARth = ring_constant "SRth_ARth"
-let coq_sring_morph = ring_constant "semi_morph"
-let coq_SRmorph_Rmorph = ring_constant "SRmorph_Rmorph"
-let coq_mk_seqe = ring_constant "mk_seqe"
-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"Ring"
-let ltac_setoid_ring_rewrite = ltac"Ring_simplify"
+let coq_semi_ring_theory = my_constant "semi_ring_theory"
+let coq_mk_seqe = my_constant "mk_seqe"
+
 let ltac_inv_morphZ = zltac"inv_gen_phiZ"
 let ltac_inv_morphN = zltac"inv_gen_phiN"
 
-
-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 rec dest_rel t =
-  match kind_of_term t with
-      App(f,args) when Array.length args >= 2 ->
-        let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
-        if closed0 rel then
-          (rel,args.(Array.length args - 2),args.(Array.length args - 1))
-        else error "ring: cannot find relation (not closed)"
-    | Prod(_,_,c) -> dest_rel c
-    | _ -> error "ring: cannot find relation"
+let coq_abstract = my_constant"Abstract"
+let coq_comp = my_constant"Computational"
+let coq_morph = my_constant"Morphism"
 
 (* Equality: do not evaluate but make recursive call on both sides *)
 let map_with_eq arg_map c =
@@ -244,7 +276,6 @@ let map_with_eq arg_map c =
   interp_map
     ((req,(function -1->Prot|_->Rec))::
     List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
-;;
 
 let _ = add_map "ring"
   (map_with_eq
@@ -255,25 +286,7 @@ let _ = add_map "ring"
     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 ty c = Typing.type_of (Global.env()) Evd.empty c
-
-let decl_constant na c =
-  mkConst(declare_constant (id_of_string na) (DefinitionEntry 
-    { const_entry_body = c;
-      const_entry_type = None;
-      const_entry_opaque = true;
-      const_entry_boxed = true}, 
-    IsProof Lemma))
-
-
-let ltac_call tac args =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+    pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -281,6 +294,10 @@ let ltac_call tac args =
 type ring_info =
     { ring_carrier : types;
       ring_req : constr;
+      ring_setoid : constr;
+      ring_ext : constr;
+      ring_morph : constr;
+      ring_th : constr;
       ring_cst_tac : glob_tactic_expr;
       ring_lemma1 : constr;
       ring_lemma2 : constr;
@@ -354,6 +371,10 @@ let add_entry (sp,_kn) e =
 let subst_th (_,subst,th) = 
   let c' = subst_mps subst th.ring_carrier in                   
   let eq' = subst_mps subst th.ring_req in
+  let set' = subst_mps subst th.ring_setoid in
+  let ext' = subst_mps subst th.ring_ext in
+  let morph' = subst_mps subst th.ring_morph in
+  let th' = subst_mps subst th.ring_th in
   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
@@ -361,6 +382,10 @@ let subst_th (_,subst,th) =
   let posttac'= subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
+     set' = th.ring_setoid &&
+     ext' == th.ring_ext &&
+     morph' == th.ring_morph &&
+     th' == th.ring_th &&
      thm1' == th.ring_lemma1 &&
      thm2' == th.ring_lemma2 &&
      tac' == th.ring_cst_tac &&
@@ -369,6 +394,10 @@ let subst_th (_,subst,th) =
   else
     { ring_carrier = c';
       ring_req = eq';
+      ring_setoid = set';
+      ring_ext = ext';
+      ring_morph = morph';
+      ring_th = th';
       ring_cst_tac = tac';
       ring_lemma1 = thm1';
       ring_lemma2 = thm2';
@@ -399,48 +428,17 @@ let op_morph r add mul opp req m1 m2 m3 =
 let op_smorph 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 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 ->
-          (th,[|c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-    | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when f = Lazy.force coq_sring_morph && kind=Some true->
-        let th =
-          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|])
-    | _ -> error "bad ring_morph lemma"
-
-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;_|] ->
-              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 default_ring_equality (r,add,mul,opp,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 _ ->
         let setoid = lapp coq_eq_setoid [|r|] in
-        let op_morph = lapp coq_eq_morph [|r;add;mul;opp|] in
+        let op_morph =
+          match opp with
+              Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
+            | None -> lapp coq_eq_smorph [|r;add;mul|] in
         (setoid,op_morph)
     | Relation rel ->
         let setoid = setoid_of_relation rel in
@@ -458,7 +456,8 @@ let default_ring_equality is_semi (r,add,mul,opp,req) =
           with Not_found ->
             error "ring multiplication should be declared as a morphism" in
         let op_morph =
-          if is_semi <> Some true then
+          match opp with
+            | Some opp ->
             (let opp_m =
               try default_morphism ~filter:is_endomorphism opp
               with Not_found ->
@@ -472,7 +471,7 @@ let default_ring_equality is_semi (r,add,mul,opp,req) =
                str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++
                str"\"");
              op_morph)
-          else
+            | None ->
             (msgnl
               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++  
                str"and morphisms \""++pr_constr add_m.morphism_theory++
@@ -481,136 +480,72 @@ let default_ring_equality is_semi (r,add,mul,opp,req) =
             op_smorph r add mul req add_m.lem mul_m.lem) in
         (setoid,op_morph)
 
-let build_setoid_params is_semi r add mul opp req eqth =
+let build_setoid_params r add mul opp req eqth =
   match eqth with
       Some th -> th
-    | None -> default_ring_equality is_semi (r,add,mul,opp,req)
+    | None -> default_ring_equality (r,add,mul,opp,req)
 
 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 ->
-          (None,r,zero,one,add,mul,sub,opp,req)
+          (None,r,zero,one,add,mul,Some sub,Some opp,req)
     | App(f,[|r;zero;one;add;mul;req|])
         when f = Lazy.force coq_semi_ring_theory ->
-        (Some true,r,zero,one,add,mul,sr_sub r add,sr_opp r,req)
+        (Some true,r,zero,one,add,mul,None,None,req)
     | App(f,[|r;zero;one;add;mul;sub;opp;req|])
         when f = Lazy.force coq_ring_theory ->
-        (Some false,r,zero,one,add,mul,sub,opp,req)
+        (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"
 
 
-let build_almost_ring kind r zero one add mul sub opp req sth morph th =
-  match kind with
-      None -> th
-    | Some true ->
-        lapp coq_SRth_ARth [|r;zero;one;add;mul;req;sth;th|]
-    | Some false ->
-        lapp coq_Rth_ARth [|r;zero;one;add;mul;sub;opp;req;sth;morph;th|]
-
 
 type coeff_spec =
     Computational of constr (* equality test *)
   | Abstract (* coeffs = Z *)
   | Morphism of constr (* general morphism *)
 
+
+let reflect_coeff rkind =
+  (* We build an ill-typed terms on purpose... *)
+  match rkind with
+      Abstract -> Lazy.force coq_abstract
+    | Computational c -> lapp coq_comp [|c|]
+    | Morphism m -> lapp coq_morph [|m|]
+
 type cst_tac_spec =
     CstTac of raw_tactic_expr
   | 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 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 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 ->
-          (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
+let interp_cst_tac kind (zero,one,add,mul,opp) 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 ->
+        (match opp, kind with
+            None, _ ->
               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 ->
+          | Some opp, Some _ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
               TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | _ -> error"a tactic must be specified for an almost_ring") in
+          | _ -> error"a tactic must be specified for an almost_ring")
+
+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,ext) = build_setoid_params r add mul opp req eqth in
+  let rk = reflect_coeff morphth in
+  let params =
+    exec_tactic env 5 (zltac"ring_lemmas") (List.map carg[sth;ext;rth;rk]) in
+  let lemma1 = constr_of params.(3) in
+  let lemma2 = constr_of params.(4) 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 = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
@@ -624,19 +559,15 @@ let add_theory name rth eqth morphth cst_tac (pre,post) =
       (theory_to_obj
         { ring_carrier = r;
           ring_req = req;
+          ring_setoid = sth;
+          ring_ext = constr_of params.(1);
+          ring_morph = constr_of params.(2);
+          ring_th = constr_of params.(0);
           ring_cst_tac = cst_tac;
           ring_lemma1 = lemma1;
           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
-*)
   ()
 
 type ring_mod =
@@ -685,73 +616,48 @@ END
 (* The tactics consist then only in a lookup in the ring database and
    call the appropriate ltac. *)
 
-let ring gl = 
-  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 make_term_list carrier rl gl =
+  let rl = 
+    match rl with
+	[] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2]
+      | _ -> rl in
+  List.fold_right
+    (fun x l -> lapp coq_cons [|carrier;x;l|]) rl
+    (lapp coq_nil [|carrier|])
 
-let ring_rewrite rl gl =
+let ring_lookup (f:glob_tactic_expr) 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
-  tclTHEN (Tacinterp.eval_tactic e.ring_pre_tac)
-    (tclTHEN
-        (fun gl ->
-	    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
-	      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])))) gl)
-	(Tacinterp.eval_tactic e.ring_post_tac)) gl
-
-TACTIC EXTEND setoid_ring
-  [ "ring" ] -> [ ring ]
-| [ "ring_simplify" constr_list(l) ] -> [ ring_rewrite l ]
+  let rl = carg (make_term_list e.ring_carrier rl gl) in
+  let req = carg e.ring_req in
+  let sth = carg e.ring_setoid in
+  let ext = carg e.ring_ext in
+  let morph = carg e.ring_morph in
+  let th = carg e.ring_th in
+  let cst_tac = Tacexp e.ring_cst_tac in
+  let lemma1 = carg e.ring_lemma1 in
+  let lemma2 = carg e.ring_lemma2 in
+  let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in
+  let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in
+  Tacinterp.eval_tactic
+    (TacLetIn
+      ([(dummy_loc,id_of_string"f"),None,Tacexp f],
+       ltac_lcall "f"
+         [req;sth;ext;morph;th;cst_tac;lemma1;lemma2;pretac;posttac;rl])) gl
+
+TACTIC EXTEND ring_lookup
+| [ "ring_lookup" tactic(f) constr_list(l) ] -> [ ring_lookup (fst f) l ]
 END
 
 (***********************************************************************)
-let fld_cst s = mk_cst [contrib_name;"Field_theory"] s ;;
-
-let field_modules = List.map
-  (fun f -> ["Coq";contrib_name;f])
-  ["Field_theory";"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
@@ -759,14 +665,14 @@ let _ = add_map "field"
     coq_nil, (function -1->Eval|_ -> Prot);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
-    fld_cst "display_linear",
+    my_constant "display_linear",
       (function -1|7|8|9|10|12|13->Eval|11->Rec|_->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);
+    my_constant "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 *)
-    fld_cst "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);;
+    my_constant "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);;
 
 
 let _ = add_map "field_cond"
@@ -775,41 +681,36 @@ let _ = add_map "field_cond"
      coq_nil, (function -1->Eval|_ -> Prot);
     (* PCond: evaluate morphism and denum list, protect ring
        operations and make recursive call on the var map *)
-     fld_cst "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);;
+     my_constant "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);;
 
 
+let afield_theory = my_constant "almost_field_theory"
+let field_theory = my_constant "field_theory"
+let sfield_theory = my_constant "semi_field_theory"
+let af_ar = my_constant"AF_AR"
+let f_r = my_constant"F_R"
+let sf_sr = my_constant"SF_SR"
 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
+        let rth = lapp af_ar
           [|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)
+        (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
         when f = Lazy.force field_theory ->
         let rth =
-          lapp (field_constant"F_R")
+          lapp 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)
+        (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
         when f = Lazy.force sfield_theory ->
-        let rth = lapp (field_constant"SF_SR")
+        let rth = lapp 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)
+        (Some true,r,zero,one,add,mul,None,None,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;
@@ -834,7 +735,7 @@ let field_lookup_by_name ref =
 
 
 let find_field_structure env sigma l cl oname =
-  check_required_library (ring_dir@["Field_tac"]);
+  check_required_library (cdir@["Field_tac"]);
   match oname, l with
       Some rf, _ ->
         (try field_lookup_by_name rf
@@ -879,15 +780,16 @@ let _ =
       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
@@ -918,7 +820,6 @@ let subst_th (_,subst,th) =
       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
@@ -949,93 +850,31 @@ let default_field_equality r inv req =
             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 (sth,ext) = build_setoid_params r add mul opp req eqth in
+  let eqth = Some(sth,ext) 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 rk = reflect_coeff morphth in
+  let params =
+    exec_tactic env 8 (field_ltac"field_lemmas")
+      (List.map carg[sth;ext;inv_m;fth;rk]) in
+  let lemma1 = constr_of params.(3) in
+  let lemma2 = constr_of params.(4) in
+  let lemma3 = constr_of params.(5) in
+  let cond_lemma =
+    match inj with
+      | Some thm -> mkApp(constr_of params.(7),[|thm|])
+      | None -> constr_of params.(6) 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 cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
         Some t -> Tacinterp.glob_tactic t
@@ -1090,51 +929,26 @@ VERNAC COMMAND EXTEND AddSetoidField
     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 field_lookup (f:glob_tactic_expr) 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
+  let rl = carg (make_term_list e.field_carrier rl gl) in
+  let req = carg e.field_req in
+  let cst_tac = Tacexp e.field_cst_tac in
+  let field_ok = carg e.field_ok in
+  let field_simpl_ok = carg e.field_simpl_ok in
+  let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
+  let cond_ok = carg e.field_cond in
+  let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in
+  let posttac = Tacexp(TacFun([None],e.field_post_tac)) 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 ]
+    (TacLetIn
+      ([(dummy_loc,id_of_string"f"),None,Tacexp f],
+       ltac_lcall "f"
+         [req;cst_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok;
+          pretac;posttac;rl])) gl
+
+TACTIC EXTEND field_lookup
+| [ "field_lookup" tactic(f) constr_list(l) ] -> [ field_lookup (fst f) l ]
 END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f7e4a9750..ee70c326f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1824,6 +1824,8 @@ and interp_genarg ist gl x =
   | BindingsArgType ->
       in_gen wit_bindings
         (interp_bindings ist gl (out_gen globwit_bindings x))
+  | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x
+  | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x
   | List0ArgType _ -> app_list0 (interp_genarg ist gl) x
   | List1ArgType _ -> app_list1 (interp_genarg ist gl) x
   | OptArgType _ -> app_opt (interp_genarg ist gl) x
@@ -1836,6 +1838,16 @@ and interp_genarg ist gl x =
       | None -> 
           lookup_interp_genarg s ist gl x
 
+and interp_genarg_constr_list0 ist gl x =
+  let lc = out_gen (wit_list0 globwit_constr) x in
+  let lc = pf_interp_constr_list ist gl lc in
+  in_gen (wit_list0 wit_constr) lc
+
+and interp_genarg_constr_list1 ist gl x =
+  let lc = out_gen (wit_list1 globwit_constr) x in
+  let lc = pf_interp_constr_list ist gl lc in
+  in_gen (wit_list1 wit_constr) lc
+
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
   let rec apply_match_subterm ist nocc (id,c) csr mt =
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index c522e01b3..18dbd27f9 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -8,15 +8,5 @@
 
 (*i $Id$ i*)
 
-Require Export Le.
-Require Export Lt.
-Require Export Plus.
-Require Export Gt.
-Require Export Minus.
-Require Export Mult.
-Require Export Between.
-Require Export Peano_dec.
-Require Export Compare_dec.
-Require Export Factorial.
-
+Require Export Arith_base.
 Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
new file mode 100644
index 000000000..b076de2af
--- /dev/null
+++ b/theories/Arith/Arith_base.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Peano_dec.
+Require Export Compare_dec.
+Require Export Factorial.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 77fa80539..6f8a5f127 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -16,7 +16,7 @@ Notation not_eq_sym := sym_not_eq.
 
 Implicit Types m n p q : nat.
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Peano_dec.
 Require Import Compare_dec.
 
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
new file mode 100644
index 000000000..d285fef30
--- /dev/null
+++ b/theories/Reals/LegacyRfield.v
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Raxioms.
+Require Export LegacyField.
+Import LegacyRing_theory.
+Open Scope R_scope.
+
+Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
+  split.
+  exact Rplus_comm.
+  symmetry  in |- *; apply Rplus_assoc.
+  exact Rmult_comm.
+  symmetry  in |- *; apply Rmult_assoc.
+  intro; apply Rplus_0_l.
+  intro; apply Rmult_1_l.
+  exact Rplus_opp_r.
+  intros.
+  rewrite Rmult_comm.
+  rewrite (Rmult_comm n p).
+  rewrite (Rmult_comm m p).
+  apply Rmult_plus_distr_l.
+  intros; contradiction.
+Defined.
+
+Add Legacy Field
+R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
+  with minus := Rminus div := Rdiv.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 1996eaa97..daebd9178 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -16,42 +16,12 @@ Require Export Raxioms.
 Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
-Require Export LegacyField.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
 
 Implicit Type r : R.
 
-(***************************************************************************)
-(** *     Instantiating Field tactic on reals                              *)
-(***************************************************************************)
-
-(* Legacy Field *)
-Require Export LegacyField.
-Import LegacyRing_theory.
-
-Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
-  split.
-  exact Rplus_comm.
-  symmetry  in |- *; apply Rplus_assoc.
-  exact Rmult_comm.
-  symmetry  in |- *; apply Rmult_assoc.
-  intro; apply Rplus_0_l.
-  intro; apply Rmult_1_l.
-  exact Rplus_opp_r.
-  intros.
-  rewrite Rmult_comm.
-  rewrite (Rmult_comm n p).
-  rewrite (Rmult_comm m p).
-  apply Rmult_plus_distr_l.
-  intros; contradiction.
-Defined.
-
-Add Legacy Field
-R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
-  with minus := Rminus div := Rdiv.
-
 (**************************************************************************)
 (** * Relation between orders and equality                                *)
 (**************************************************************************)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index db995f3b0..f048faf53 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -397,15 +397,14 @@ Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.
 Proof.
   intro; induction  n as [| n Hrecn].
   reflexivity.
-  replace (2 * S n)%nat with (2 + 2 * n)%nat.
+  replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.
   rewrite pow_add; rewrite Hrecn; simpl in |- *; ring.
-  replace (S n) with (n + 1)%nat; [ ring | ring ].
 Qed.
 
 (**********)
 Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.
 Proof.
-  intro; replace (S (2 * n)) with (2 * n + 1)%nat; [ idtac | ring ].
+  intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring.
   rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring.
 Qed.
 
@@ -425,7 +424,7 @@ Proof.
   intros; induction  n2 as [| n2 Hrecn2].
   simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
   replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.
-  replace (S n2) with (n2 + 1)%nat; [ idtac | ring ].
+  replace (S n2) with (n2 + 1)%nat by ring.
   do 2 rewrite pow_add.
   rewrite Hrecn2.
   simpl in |- *.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index f648867aa..c7f0bb723 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -9,7 +9,7 @@
 
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import BinPos.
 Require Import BinInt.
 Require Import Zorder.
@@ -127,4 +127,4 @@ Proof.
   compute in |- *. intro H0. discriminate H0. intuition.
 
   intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index ca647ff3c..b2c068564 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import BinInt.
 Require Import Zcompare.
 Require Import Zorder.
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index a1e46fa5f..0e0caa1bd 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -12,7 +12,7 @@
     from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
  *)
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import BinInt.
 Require Import Zcompare.
 Require Import Zorder.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 8a18798c2..27f31bf83 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -10,7 +10,7 @@
 
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
-Require Export Arith.
+Require Export Arith_base.
 Require Import BinPos.
 Require Import BinInt.
 Require Import Zcompare.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index e26754505..4b0d2562e 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -11,7 +11,7 @@
 
 Require Import BinPos.
 Require Import BinInt.
-Require Import Arith.
+Require Import Arith_base.
 Require Import Decidable.
 Require Import Zcompare.
 
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index c6b398110..18b49f4bb 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -10,7 +10,7 @@
 
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
-Require Export Arith.
+Require Export Arith_base.
 Require Import BinInt.
 Require Import Zorder.
 Require Import Decidable.