commit de field + renommages

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

33 files changed, 2124 insertions, 78 deletions

diff --git a/.depend.coq b/.depend.coq
index af7a8d9ca..59ad870a6 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -28,7 +28,7 @@ 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/NewZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/Field_tac.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/Field_tac.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/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
@@ -36,8 +36,8 @@ theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.v
 theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
 theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
 theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/NewArithRing.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/ArithRing.vo contrib/setoid_ring/NewArithRing.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
 theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
 theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
@@ -173,14 +173,14 @@ 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
 theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo
 theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
-theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v contrib/setoid_ring/NewZArithRing.vo theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo theories/Lists/List.vo
-theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo theories/ZArith/Zbool.vo contrib/omega/Omega.vo contrib/setoid_ring/NewZArithRing.vo theories/ZArith/Zcomplements.vo
-theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v contrib/setoid_ring/NewZArithRing.vo contrib/omega/Omega.vo theories/ZArith/ZArith_base.vo
+theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v contrib/setoid_ring/ZArithRing.vo theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo theories/Lists/List.vo
+theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo theories/ZArith/Zbool.vo contrib/omega/Omega.vo contrib/setoid_ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
+theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo theories/ZArith/ZArith_base.vo
 theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo theories/Arith/Wf_nat.vo contrib/omega/Omega.vo
 theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo theories/ZArith/Zcompare.vo theories/ZArith/Zorder.vo theories/ZArith/Zeven.vo theories/ZArith/Zmin.vo theories/ZArith/Zmax.vo theories/ZArith/Zminmax.vo theories/ZArith/Zabs.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zbool.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
 theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/BinInt.vo theories/ZArith/Zeven.vo theories/ZArith/Zorder.vo theories/ZArith/Zcompare.vo theories/ZArith/ZArith_dec.vo theories/Bool/Sumbool.vo
 theories/ZArith/Zbinary.vo: theories/ZArith/Zbinary.v theories/Bool/Bvector.vo theories/ZArith/ZArith.vo theories/ZArith/Zpower.vo contrib/omega/Omega.vo
-theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/setoid_ring/NewZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo theories/NArith/Ndigits.vo theories/Arith/Wf_nat.vo
+theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/setoid_ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo theories/NArith/Ndigits.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Int.vo: theories/ZArith/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Relations/Relation_Definitions.vo
 theories/Lists/MonoList.vo: theories/Lists/MonoList.v theories/Arith/Le.vo
@@ -271,7 +271,7 @@ 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/NewZArithRing.vo contrib/omega/Omega.vo contrib/setoid_ring/Field_tac.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/Field_tac.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/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
@@ -279,8 +279,8 @@ theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.v
 theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
 theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
 theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/NewArithRing.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/ArithRing.vo contrib/setoid_ring/NewArithRing.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
 theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
 theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
 theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
@@ -327,30 +327,30 @@ theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relatio
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
 theories/Sorting/PermutSetoid.vo: theories/Sorting/PermutSetoid.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Lists/SetoidList.vo
 theories/Sorting/PermutEq.vo: theories/Sorting/PermutEq.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Setoids/Setoid.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo
-theories/QArith/QArith_base.vo: theories/QArith/QArith_base.v theories/ZArith/ZArith.vo contrib/setoid_ring/NewZArithRing.vo theories/Setoids/Setoid.vo
+theories/QArith/QArith_base.vo: theories/QArith/QArith_base.v theories/ZArith/ZArith.vo contrib/setoid_ring/ZArithRing.vo theories/Setoids/Setoid.vo
 theories/QArith/Qreduction.vo: theories/QArith/Qreduction.v theories/QArith/QArith_base.vo theories/ZArith/Znumtheory.vo
 theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/setoid_ring/Ring.vo theories/QArith/QArith_base.vo
 theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo
 theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo
-theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/NewField.vo contrib/setoid_ring/Field_tac.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo
+theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/Field.vo contrib/setoid_ring/Field_tac.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo
 contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo
 contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo
 contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/romega/ReflOmegaCore.vo
-contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
-contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
-contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
-contrib/ring/LegacyRing.vo: contrib/ring/LegacyRing.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
-contrib/ring/NArithRing.vo: contrib/ring/NArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/ZArith/ZArith_base.vo theories/NArith/NArith.vo theories/Logic/Eqdep_dec.vo
-contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo
-contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
+contrib/ring/LegacyArithRing.vo: contrib/ring/LegacyArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo
+contrib/ring/LegacyRing_theory.vo: contrib/ring/LegacyRing_theory.v theories/Bool/Bool.vo
+contrib/ring/LegacyRing.vo: contrib/ring/LegacyRing.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo
+contrib/ring/LegacyNArithRing.vo: contrib/ring/LegacyNArithRing.v theories/Bool/Bool.vo contrib/ring/LegacyRing.vo theories/ZArith/ZArith_base.vo theories/NArith/NArith.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/LegacyZArithRing.vo: contrib/ring/LegacyZArithRing.v contrib/setoid_ring/ArithRing.vo theories/ZArith/ZArith_base.vo theories/Logic/Eqdep_dec.vo
+contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/LegacyRing_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
 contrib/ring/Quote.vo: contrib/ring/Quote.v
 contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo
 contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo
 contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v theories/Lists/List.vo
 contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/LegacyRing.vo contrib/field/Field_Compl.vo
-contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.vo contrib/setoid_ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
+contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.vo contrib/ring/LegacyRing.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo
 contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
 contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo
@@ -360,16 +360,13 @@ contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theor
 contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo
 contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 contrib/setoid_ring/BinList.vo: contrib/setoid_ring/BinList.v theories/NArith/BinPos.vo theories/Lists/List.vo
-contrib/setoid_ring/Ring_th.vo: contrib/setoid_ring/Ring_th.v theories/Setoids/Setoid.vo
-contrib/setoid_ring/Pol.vo: contrib/setoid_ring/Pol.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_th.vo
-contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Pol.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/newring.cmo
-contrib/setoid_ring/ZRing_th.vo: contrib/setoid_ring/ZRing_th.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/Pol.vo
-contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Ring_theory.vo contrib/ring/Setoid_ring_theory.vo contrib/setoid_ring/Ring_th.vo
-contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_th.vo contrib/setoid_ring/Ring_tac.vo
-contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_th.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/ZRing_th.vo contrib/setoid_ring/Ring_equiv.vo
-contrib/setoid_ring/NewArithRing.vo: contrib/setoid_ring/NewArithRing.v theories/Arith/Arith.vo contrib/setoid_ring/Ring.vo
-contrib/setoid_ring/NewNArithRing.vo: contrib/setoid_ring/NewNArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.vo
-contrib/setoid_ring/NewZArithRing.vo: contrib/setoid_ring/NewZArithRing.v contrib/setoid_ring/Ring.vo
-contrib/setoid_ring/NewField.vo: contrib/setoid_ring/NewField.v contrib/setoid_ring/Pol.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo contrib/setoid_ring/ZRing_th.vo
-contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/ZRing_th.vo contrib/setoid_ring/NewField.vo
-contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v contrib/setoid_ring/Pol.vo contrib/setoid_ring/ZRing_th.vo contrib/setoid_ring/NewField.vo contrib/setoid_ring/Field_tac.vo contrib/setoid_ring/Ring.vo theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.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_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_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/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/Ring_equiv.vo
+contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Arith.vo contrib/setoid_ring/Ring.vo
+contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.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.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
+contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field.vo
+contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field.vo contrib/setoid_ring/Field_tac.vo contrib/setoid_ring/Ring.vo theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo
diff --git a/Makefile b/Makefile
index 7a7725c52..40a46316a 100644
--- a/Makefile
+++ b/Makefile
@@ -1035,22 +1035,22 @@ ROMEGAVO=\
  contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo 
 
 RINGVO=\
- contrib/ring/ArithRing.vo      contrib/ring/Ring_normalize.vo \
- contrib/ring/Ring_theory.vo    contrib/ring/LegacyRing.vo \
- contrib/ring/NArithRing.vo     \
- contrib/ring/ZArithRing.vo     contrib/ring/Ring_abstract.vo \
- contrib/ring/Quote.vo		contrib/ring/Setoid_ring_normalize.vo \
- contrib/ring/Setoid_ring.vo	contrib/ring/Setoid_ring_theory.vo
+ contrib/ring/LegacyArithRing.vo      	contrib/ring/Ring_normalize.vo \
+ contrib/ring/LegacyRing_theory.vo	contrib/ring/LegacyRing.vo \
+ contrib/ring/LegacyNArithRing.vo     \
+ contrib/ring/LegacyZArithRing.vo	contrib/ring/Ring_abstract.vo \
+ contrib/ring/Quote.vo			contrib/ring/Setoid_ring_normalize.vo \
+ contrib/ring/Setoid_ring.vo		contrib/ring/Setoid_ring_theory.vo
 
 NEWRINGVO=\
  contrib/setoid_ring/BinList.vo   contrib/setoid_ring/Ring_th.vo \
  contrib/setoid_ring/Pol.vo       contrib/setoid_ring/Ring_tac.vo \
  contrib/setoid_ring/ZRing_th.vo  contrib/setoid_ring/Ring_equiv.vo \
  contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring.vo \
- contrib/setoid_ring/NewArithRing.vo \
- contrib/setoid_ring/NewNArithRing.vo \
- contrib/setoid_ring/NewZArithRing.vo \
-contrib/setoid_ring/NewField.vo \
+ contrib/setoid_ring/ArithRing.vo \
+ contrib/setoid_ring/NArithRing.vo \
+ contrib/setoid_ring/ZArithRing.vo \
+contrib/setoid_ring/Field.vo \
 contrib/setoid_ring/Field_tac.vo \
 contrib/setoid_ring/RealField.vo
 
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/LegacyArithRing.v
index 959d66c74..959d66c74 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/LegacyArithRing.v
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/LegacyNArithRing.v
index ee9fb3761..ee9fb3761 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/LegacyNArithRing.v
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index 667e24d53..dc8635bdf 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -9,7 +9,7 @@
 (* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Bool.
-Require Export Ring_theory.
+Require Export LegacyRing_theory.
 Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/LegacyRing_theory.v
index 192ff1f57..192ff1f57 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/LegacyRing_theory.v
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/LegacyZArithRing.v
index 075431827..075431827 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/LegacyZArithRing.v
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 574c24421..28de54e65 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Import Ring_theory.
+Require Import LegacyRing_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 6d0d05778..199ae7572 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Import Ring_theory.
+Require Import LegacyRing_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 1c5121ef6..e81c9ddd5 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -43,7 +43,7 @@ let ring_dir = ["Coq";"ring"]
 let setoids_dir = ["Coq";"Setoids"]
 
 let ring_constant = Coqlib.gen_constant_in_modules "Ring"
-  [ring_dir@["Ring_theory"];
+  [ring_dir@["LegacyRing_theory"];
    ring_dir@["Setoid_ring_theory"];
    ring_dir@["Ring_normalize"];
    ring_dir@["Ring_abstract"];
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
new file mode 100644
index 000000000..bd4c6062c
--- /dev/null
+++ b/contrib/setoid_ring/ArithRing.v
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  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 Arith.
+Require Export Ring.
+Set Implicit Arguments.
+
+Ltac isnatcst t :=
+  let t := eval hnf in t in
+  match t with
+    O => true
+  | S ?p => isnatcst p
+  | _ => false
+  end.
+Ltac natcst t :=
+  match isnatcst t with
+    true => t
+  | _ => NotConstant
+  end.
+
+Ltac natprering :=
+  match goal with
+    |- context C [S ?p] =>
+    match p with
+      O => fail 1 (* avoid replacing 1 with 1+0 ! *)
+    | S _ => fail 1
+    | _ => fold (1+p)%nat; natprering
+    end
+  | _ => idtac
+  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 Ring natr : natSRth
+  (decidable nateq_ok, constants [natcst], preprocess [natprering]).
diff --git a/contrib/setoid_ring/Field.v b/contrib/setoid_ring/Field.v
new file mode 100644
index 000000000..63a94a178
--- /dev/null
+++ b/contrib/setoid_ring/Field.v
@@ -0,0 +1,1193 @@
+(************************************************************************)
+(*  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 Ring.
+Export Ring_polynom.
+Import Ring_theory InitialRing Setoid List.
+Require Import ZArith_base.
+
+Section MakeFieldPol.
+
+(* Field elements *)     
+ Variable R:Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
+ Variable (rdiv : R -> R ->  R) (rinv : 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 / y" := (rdiv x y).
+ Notation "- x" := (ropp x). Notation "/ x" := (rinv x).
+ Notation "x == y" := (req x y) (at level 70, no associativity).
+
+ (* Equality properties *)
+ Variable Rsth : Setoid_Theory R req.
+ Variable Reqe : ring_eq_ext radd rmul ropp req.
+ Variable SRinv_ext : forall p q, p == q ->  / p == / q.
+
+ (* Field properties *)
+  Record almost_field_theory : Prop := mk_afield {
+    AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req;
+    AF_1_neq_0 : ~ 1 == 0;
+    AFdiv_def : forall p q, p / q == p * / q;
+    AFinv_l : forall p, ~ p == 0 ->  / p * p == 1
+  }.
+
+Section AlmostField.
+
+ Variable AFth : almost_field_theory.
+ Let ARth := AFth.(AF_AR).
+ Let rI_neq_rO := AFth.(AF_1_neq_0).
+ Let rdiv_def := AFth.(AFdiv_def).
+ Let rinv_l := AFth.(AFinv_l).
+
+ (* Coefficients *) 
+ Variable C: Type.
+ Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
+ Variable ceqb : C->C->bool. 
+ Variable phi : C -> R.
+
+ Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
+                               cO cI cadd cmul csub copp ceqb phi.
+
+Lemma ceqb_rect : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
+  (phi c1 == phi c2 -> P x) -> P y -> P (if ceqb c1 c2 then x else y).
+Proof.
+intros.
+generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
+case (ceqb c1 c2); auto.
+Qed.
+
+
+ (* C notations *)		 
+ Notation "x +! y" := (cadd x y) (at level 50).
+ Notation "x *! y " := (cmul x y) (at level 40).
+ Notation "x -! y " := (csub x y) (at level 50).
+ Notation "-! x" := (copp x) (at level 35).
+ Notation " x ?=! y" := (ceqb x y) (at level 70, no associativity).
+ Notation "[ x ]" := (phi x) (at level 0).
+
+
+ (* Usefull tactics *)		  
+  Add Setoid R req Rsth as R_set1.
+  Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
+  Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
+  Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
+  Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+  Add Morphism rinv : rinv_ext. exact SRinv_ext. Qed.
+ 
+Let eq_trans := Setoid.Seq_trans _ _ Rsth.
+Let eq_sym := Setoid.Seq_sym _ _ Rsth.
+Let eq_refl := Setoid.Seq_refl _ _ Rsth.
+
+Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) .
+Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe)
+             (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext.
+Hint Resolve (ARadd_0_l  ARth) (ARadd_sym  ARth) (ARadd_assoc ARth)
+             (ARmul_1_l  ARth) (ARmul_0_l  ARth) 
+             (ARmul_sym  ARth) (ARmul_assoc ARth) (ARdistr_l  ARth)
+             (ARopp_mul_l ARth) (ARopp_add  ARth) 
+             (ARsub_def  ARth) .
+
+Notation NPEeval := (PEeval rO radd rmul rsub ropp phi).
+Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb).
+Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi).
+
+(* add abstract semi-ring to help with some proofs *)
+Add Ring Rring : (ARth_SRth ARth).
+
+
+(* additional ring properties *)
+
+Lemma rsub_0_l : forall r, 0 - r == - r.
+intros; rewrite (ARsub_def ARth) in |- *; ring.
+Qed.
+
+Lemma rsub_0_r : forall r, r - 0 == r.
+intros; rewrite (ARsub_def ARth) in |- *.
+rewrite (ARopp_zero Rsth Reqe ARth) in |- *;  ring.
+Qed.
+
+(***************************************************************************
+                                                                          
+                       Properties of division                             
+                                                                          
+  ***************************************************************************)
+ 
+Theorem rdiv_simpl: forall p q, ~ q == 0 ->  q * (p / q) == p.
+intros p q H.
+rewrite rdiv_def in |- *.
+transitivity (/ q * q * p); [  ring | idtac ].
+rewrite rinv_l in |- *; auto.
+Qed.
+Hint Resolve rdiv_simpl .
+ 
+Theorem SRdiv_ext:
+ forall p1 p2, p1 == p2 -> forall q1 q2, q1 == q2 ->  p1 / q1 == p2 / q2.
+intros p1 p2 H q1 q2 H0.
+transitivity (p1 * / q1); auto.
+transitivity (p2 * / q2); auto.
+Qed.
+Hint Resolve SRdiv_ext .
+
+ Add Morphism rdiv : rdiv_ext. exact SRdiv_ext. Qed.
+
+Lemma rmul_reg_l : forall p q1 q2,
+  ~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
+intros.
+rewrite <- (rdiv_simpl q1 p) in |- *; trivial.
+rewrite <- (rdiv_simpl q2 p) in |- *; trivial.
+repeat rewrite rdiv_def in |- *.
+repeat rewrite (ARmul_assoc ARth) in |- *.
+auto.
+Qed.
+
+Theorem field_is_integral_domain : forall r1 r2,
+  ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
+Proof.
+red in |- *; intros.
+apply H0.
+transitivity (1 * r2); auto.
+transitivity (/ r1 * r1 * r2); auto.
+rewrite <- (ARmul_assoc ARth) in |- *.
+rewrite H1 in |- *.
+apply ARmul_0_r with (1 := Rsth) (2 := ARth).
+Qed.
+
+Theorem ropp_neq_0 : forall r,
+  ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0.
+intros.
+setoid_replace (- r) with (- (1) * r).
+ apply field_is_integral_domain; trivial.
+ rewrite <- (ARopp_mul_l ARth) in |- *.
+   rewrite (ARmul_1_l ARth) in |- *.
+   reflexivity.
+Qed.
+
+Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1.
+intros.
+rewrite (AFdiv_def AFth) in |- *.
+rewrite (ARmul_sym ARth) in |- *.
+apply (AFinv_l AFth).
+trivial.
+Qed.
+
+Theorem rdiv1: forall r,  r == r / 1.
+intros r; transitivity (1 * (r / 1)); auto.
+Qed.
+ 
+Theorem rdiv2:
+ forall r1 r2 r3 r4,
+ ~ r2 == 0 ->
+ ~ r4 == 0 ->
+ r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
+Proof.
+intros r1 r2 r3 r4 H H0.
+assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
+apply rmul_reg_l with (r2 * r4); trivial.
+rewrite rdiv_simpl in |- *; trivial.
+rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+apply (Radd_ext Reqe).
+ transitivity (r2 * (r1 / r2) * r4); [  ring | auto ].
+ transitivity (r2 * (r4 * (r3 / r4))); auto.
+   transitivity (r2 * r3); auto.
+Qed.
+
+Theorem rdiv5: forall r1 r2,  - (r1 / r2) == - r1 / r2.
+intros r1 r2.
+transitivity (- (r1 * / r2)); auto.
+transitivity (- r1 * / r2); auto.
+Qed.
+Hint Resolve rdiv5 .
+
+Theorem rdiv3:
+ forall r1 r2 r3 r4,
+ ~ r2 == 0 ->
+ ~ r4 == 0 ->
+ r1 / r2 - r3 / r4 == (r1 * r4 -  r3 * r2) / (r2 * r4).
+intros r1 r2 r3 r4 H H0.
+assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
+transitivity (r1 / r2 + - (r3 / r4)); auto.
+transitivity (r1 / r2 + - r3 / r4); auto.
+transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)); auto.
+apply rdiv2; auto.
+apply SRdiv_ext; auto.
+transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
+Qed.
+
+Theorem rdiv6:
+ forall r1 r2,
+ ~ r1 == 0 -> ~ r2 == 0 ->  / (r1 / r2) == r2 / r1.
+intros r1 r2 H H0.
+assert (~ r1 / r2 == 0) as Hk.
+ intros H1; case H.
+   transitivity (r2 * (r1 / r2)); auto.
+   rewrite H1 in |- *;  ring.
+ apply rmul_reg_l with (r1 / r2); auto.
+   transitivity (/ (r1 / r2) * (r1 / r2)); auto.
+   transitivity 1; auto.
+   repeat rewrite rdiv_def in |- *.
+   transitivity (/ r1 * r1 * (/ r2 * r2)); [ idtac |  ring ].
+   repeat rewrite rinv_l in |- *; auto.
+Qed.
+Hint Resolve rdiv6 .
+ 
+ Theorem rdiv4:
+ forall r1 r2 r3 r4,
+ ~ r2 == 0 ->
+ ~ r4 == 0 ->
+ (r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
+Proof.
+intros r1 r2 r3 r4 H H0.
+assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
+apply rmul_reg_l with (r2 * r4); trivial.
+rewrite rdiv_simpl in |- *; trivial.
+transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [  ring | idtac ].
+repeat rewrite rdiv_simpl in |- *; trivial.
+Qed.
+
+ Theorem rdiv7:
+ forall r1 r2 r3 r4,
+ ~ r2 == 0 ->
+ ~ r3 == 0 ->
+ ~ r4 == 0 ->
+ (r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3).
+Proof.
+intros.
+rewrite (rdiv_def (r1 / r2)) in |- *.
+rewrite rdiv6 in |- *; trivial.
+apply rdiv4; trivial.
+Qed.
+
+Theorem rdiv8: forall r1 r2, ~ r2 == 0 -> r1 == 0 ->  r1 / r2 == 0.
+intros r1 r2 H H0.
+transitivity (r1 * / r2); auto.
+transitivity (0 * / r2); auto.
+Qed.
+
+
+Theorem cross_product_eq : forall r1 r2 r3 r4,
+  ~ r2 == 0 -> ~ r4 == 0 -> r1 * r4 == r3 * r2 -> r1 / r2 == r3 / r4.
+intros.
+transitivity (r1 / r2 * (r4 / r4)).
+ rewrite rdiv_r_r in |- *; trivial.
+   symmetry  in |- *.
+   apply (ARmul_1_r Rsth ARth).
+ rewrite rdiv4 in |- *; trivial.
+   rewrite H1 in |- *.
+   rewrite (ARmul_sym ARth r2 r4) in |- *.
+   rewrite <- rdiv4 in |- *; trivial.
+   rewrite rdiv_r_r in |- *.
+  trivial.
+  apply (ARmul_1_r Rsth ARth).
+Qed.
+
+(***************************************************************************
+                                                                          
+                       Some equality test                             
+                                                                          
+  ***************************************************************************)
+
+Fixpoint positive_eq (p1 p2 : positive) {struct p1} : bool :=
+ match p1, p2 with
+   xH, xH => true
+  | xO p3, xO p4 => positive_eq p3 p4
+  | xI p3, xI p4 => positive_eq p3 p4
+  | _, _ => false
+ end.
+ 
+Theorem positive_eq_correct:
+ forall p1 p2,  if positive_eq p1 p2 then p1 = p2 else p1 <> p2.
+intros p1; elim p1;
+ (try (intros p2; case p2; simpl; auto; intros; discriminate)).
+intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
+generalize (rec p4); case (positive_eq p3 p4); auto.
+intros H1; apply f_equal with ( f := xI ); auto.
+intros H1 H2; case H1; injection H2; auto.
+intros p3 rec p2; case p2; simpl; auto; (try (intros; discriminate)); intros p4.
+generalize (rec p4); case (positive_eq p3 p4); auto.
+intros H1; apply f_equal with ( f := xO ); auto.
+intros H1 H2; case H1; injection H2; auto.
+Qed.
+ 
+(* equality test *)
+Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
+ match e1, e2 with
+   PEc c1, PEc c2 => ceqb c1 c2
+  | PEX p1, PEX p2 => positive_eq p1 p2
+  | PEadd e3 e5, PEadd e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
+  | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
+  | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
+  | PEopp e3, PEopp e4 => PExpr_eq e3 e4
+  | _, _ => false
+ end.
+ 
+Theorem PExpr_eq_semi_correct:
+ forall l e1 e2, PExpr_eq e1 e2 = true ->  NPEeval l e1 == NPEeval l e2.
+intros l e1; elim e1.
+intros c1; intros e2; elim e2; simpl; (try (intros; discriminate)).
+intros c2; apply (morph_eq CRmorph).
+intros p1; intros e2; elim e2; simpl; (try (intros; discriminate)).
+intros p2; generalize (positive_eq_correct p1 p2); case (positive_eq p1 p2);
+ (try (intros; discriminate)); intros H; rewrite H; auto.
+intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
+intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
+ (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
+ (try (intros; discriminate)); auto.
+intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
+intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
+ (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
+ (try (intros; discriminate)); auto.
+intros e3 rec1 e5 rec2 e2; case e2; simpl; (try (intros; discriminate)).
+intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4);
+ (try (intros; discriminate)); generalize (rec2 e6); case (PExpr_eq e5 e6);
+ (try (intros; discriminate)); auto.
+intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))).
+intros e4; generalize (rec e4); case (PExpr_eq e3 e4);
+ (try (intros; discriminate)); auto.
+Qed.
+
+(* add *)
+Definition NPEadd e1 e2 :=
+  match e1, e2 with
+    PEc c1, PEc c2 => PEc (cadd c1 c2)
+  | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2
+  |  _, PEc c => if ceqb c cO then e1 else PEadd e1 e2
+  | _, _ => PEadd e1 e2
+  end.
+
+Theorem NPEadd_correct:
+ forall l e1 e2, NPEeval l (NPEadd e1 e2) == NPEeval l (PEadd e1 e2).
+Proof.
+intros l e1 e2.
+destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
+ try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
+ try rewrite (morph0 CRmorph) in |- *; try ring.
+apply (morph_add CRmorph).
+Qed.
+
+(* mul *) 
+Definition NPEmul x y :=
+  match x, y with
+    PEc c1, PEc c2 => PEc (cmul c1 c2)
+  | PEc c, _ =>
+      if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y
+  |  _, PEc c =>
+      if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
+  |  _, _ => PEmul x y
+  end.
+             
+Theorem NPEmul_correct : forall l e1 e2,
+  NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2).
+intros l e1 e2.
+destruct e1; destruct e2; simpl in |- *; try reflexivity;
+ repeat apply ceqb_rect;
+ try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
+ try rewrite (morph0 CRmorph) in |- *;
+ try rewrite (morph1 CRmorph) in |- *;
+ try ring.
+apply (morph_mul CRmorph).
+Qed.
+
+(* sub *)
+Definition NPEsub e1 e2 :=
+  match e1, e2 with
+    PEc c1, PEc c2 => PEc (csub c1 c2)
+  | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2
+  |  _, PEc c => if ceqb c cO then e1 else PEsub e1 e2
+  | _, _ => PEsub e1 e2
+  end.
+
+Theorem NPEsub_correct:
+ forall l e1 e2,  NPEeval l (NPEsub e1 e2) == NPEeval l (PEsub e1 e2).
+intros l e1 e2.
+destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect;
+ try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;
+ try rewrite (morph0 CRmorph) in |- *; try reflexivity;
+ try (symmetry; apply rsub_0_l); try (symmetry; apply rsub_0_r).
+apply (morph_sub CRmorph).
+Qed.
+ 
+(* opp *)
+Definition NPEopp e1 :=
+  match e1 with PEc c1 => PEc (copp c1) | _ => PEopp e1 end.
+ 
+Theorem NPEopp_correct:
+ forall l e1,  NPEeval l (NPEopp e1) == NPEeval l (PEopp e1).
+intros l e1; case e1; simpl; auto.
+intros; apply (morph_opp CRmorph).
+Qed.
+ 
+(* simplification *)
+Fixpoint PExpr_simp (e : PExpr C) : PExpr C :=
+ match e with
+   PEadd e1 e2 => NPEadd (PExpr_simp e1) (PExpr_simp e2)
+  | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2)
+  | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2)
+  | PEopp e1 => NPEopp (PExpr_simp e1)
+  | _ => e
+ end.
+ 
+Theorem PExpr_simp_correct:
+ forall l e,  NPEeval l (PExpr_simp e) == NPEeval l e.
+intros l e; elim e; simpl; auto.
+intros e1 He1 e2 He2.
+transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto.
+apply NPEadd_correct.
+simpl; auto.
+intros e1 He1 e2 He2.
+transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))); auto.
+apply NPEsub_correct.
+simpl; auto.
+intros e1 He1 e2 He2.
+transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto.
+apply NPEmul_correct.
+simpl; auto.
+intros e1 He1.
+transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto.
+apply NPEopp_correct.
+simpl; auto.
+Qed.
+
+
+(****************************************************************************
+                                                                          
+                               Datastructure                              
+                                                                          
+  ***************************************************************************)
+
+(* The input: syntax of a field expression *)
+
+Inductive FExpr : Type :=
+   FEc: C ->  FExpr
+ | FEX: positive ->  FExpr
+ | FEadd: FExpr -> FExpr ->  FExpr
+ | FEsub: FExpr -> FExpr ->  FExpr
+ | FEmul: FExpr -> FExpr ->  FExpr
+ | FEopp: FExpr ->  FExpr
+ | FEinv: FExpr ->  FExpr
+ | FEdiv: FExpr -> FExpr ->  FExpr .
+
+Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
+  match pe with
+  | FEc c     => phi c
+  | FEX x     => BinList.nth 0 x l
+  | FEadd x y => FEeval l x + FEeval l y
+  | FEsub x y => FEeval l x - FEeval l y
+  | FEmul x y => FEeval l x * FEeval l y
+  | FEopp x   => - FEeval l x
+  | FEinv x   => / FEeval l x
+  | FEdiv x y => FEeval l x / FEeval l y
+  end.
+
+(* The result of the normalisation *)
+ 
+Record linear : Type := mk_linear {
+   num : PExpr C;
+   denum : PExpr C;
+   condition : list (PExpr C) }.
+
+(***************************************************************************
+
+                Semantics and properties of side condition
+
+  ***************************************************************************)
+ 
+Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop :=
+  match le with
+  | nil => True
+  | e1 :: nil => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO
+  | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO /\ PCond l l1
+  end.
+
+Theorem PCond_cons_inv_l :
+   forall l a l1, PCond l (a::l1) ->  ~ NPEeval l a == 0.
+intros l a l1 H.
+destruct l1; simpl in H |- *; trivial.
+destruct H; trivial.
+Qed.
+ 
+Theorem PCond_cons_inv_r : forall l a l1, PCond l (a :: l1) ->  PCond l l1.
+intros l a l1 H.
+destruct l1; simpl in H |- *; trivial.
+destruct H; trivial.
+Qed.
+
+Theorem PCond_app_inv_l: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l1.
+intros l l1 l2; elim l1; simpl app in |- *.
+ simpl in |- *; auto.
+ destruct l0; simpl in *.
+  destruct l2; firstorder.
+  firstorder.
+Qed.
+ 
+Theorem PCond_app_inv_r: forall l l1 l2, PCond l (l1 ++ l2) ->  PCond l l2.
+intros l l1 l2; elim l1; simpl app; auto.
+intros a l0 H H0; apply H; apply PCond_cons_inv_r with ( 1 := H0 ).
+Qed.
+ 
+(* An unsatisfiable condition: issued when a division by zero is detected *)
+Definition absurd_PCond := cons (PEc cO) nil.
+
+Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
+unfold absurd_PCond in |- *; simpl in |- *.
+red in |- *; intros.
+apply H.
+apply (morph0 CRmorph).
+Qed.
+
+(***************************************************************************
+                                                                          
+                               Normalisation                              
+                                                                          
+  ***************************************************************************)
+
+Fixpoint Fnorm (e : FExpr) : linear :=
+  match e with
+  | FEc c => mk_linear (PEc c) (PEc cI) nil
+  | FEX x => mk_linear (PEX C x) (PEc cI) nil
+  | FEadd e1 e2 =>
+      let x := Fnorm e1 in
+      let y := Fnorm e2 in
+      mk_linear
+        (NPEadd (NPEmul (num x) (denum y)) (NPEmul (num y) (denum x)))
+        (NPEmul (denum x) (denum y))
+        (condition x ++ condition y)
+  | FEsub e1 e2 =>
+      let x := Fnorm e1 in
+      let y := Fnorm e2 in
+      mk_linear
+        (NPEsub (NPEmul (num x) (denum y))
+                (NPEmul (num y) (denum x)))
+        (NPEmul (denum x) (denum y))
+        (condition x ++ condition y)
+  | FEmul e1 e2 =>
+      let x := Fnorm e1 in
+      let y := Fnorm e2 in
+      mk_linear (NPEmul (num x) (num y))
+        (NPEmul (denum x) (denum y))
+        (condition x ++ condition y)
+  | FEopp e1 =>
+      let x := Fnorm e1 in
+      mk_linear (NPEopp (num x)) (denum x) (condition x)
+  | FEinv e1 =>
+      let x := Fnorm e1 in
+      mk_linear (denum x) (num x) (num x :: condition x)
+  | FEdiv e1 e2 =>
+      let x := Fnorm e1 in
+      let y := Fnorm e2 in
+      mk_linear (NPEmul (num x) (denum y))
+        (NPEmul (denum x) (num y))
+        (num y :: condition x ++ condition y)
+  end.
+
+
+(* Example *)
+(*
+Eval compute
+   in (Fnorm
+        (FEdiv
+          (FEc cI)
+          (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))).
+*)
+
+Theorem Pcond_Fnorm:
+ forall l e,
+ PCond l (condition (Fnorm e)) ->  ~ NPEeval l (denum (Fnorm e)) == 0.
+intros l e; elim e.
+ simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO.
+ simpl in |- *; intros _ _; rewrite (morph1 CRmorph) in |- *; exact rI_neq_rO.
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl condition in Hcond.
+   simpl denum in |- *.
+   rewrite NPEmul_correct in |- *.
+   simpl in |- *.
+   apply field_is_integral_domain.
+  apply Hrec1.
+    apply PCond_app_inv_l with (1 := Hcond).
+  apply Hrec2.
+    apply PCond_app_inv_r with (1 := Hcond).
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl condition in Hcond.
+   simpl denum in |- *.
+   rewrite NPEmul_correct in |- *.
+   simpl in |- *.
+   apply field_is_integral_domain.
+  apply Hrec1.
+    apply PCond_app_inv_l with (1 := Hcond).
+  apply Hrec2.
+    apply PCond_app_inv_r with (1 := Hcond).
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl condition in Hcond.
+   simpl denum in |- *.
+   rewrite NPEmul_correct in |- *.
+   simpl in |- *.
+   apply field_is_integral_domain.
+  apply Hrec1.
+    apply PCond_app_inv_l with (1 := Hcond).
+  apply Hrec2.
+    apply PCond_app_inv_r with (1 := Hcond).
+ intros e1 Hrec1 Hcond.
+   simpl condition in Hcond.
+   simpl denum in |- *.
+   auto.
+ intros e1 Hrec1 Hcond.
+   simpl condition in Hcond.
+   simpl denum in |- *.
+   apply PCond_cons_inv_l with (1:=Hcond).
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl condition in Hcond.
+   simpl denum in |- *.
+   rewrite NPEmul_correct in |- *.
+   simpl in |- *.
+   apply field_is_integral_domain.
+  apply Hrec1.
+    specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
+    apply PCond_app_inv_l with (1 := Hcond1).
+   apply PCond_cons_inv_l with (1:=Hcond).
+Qed.
+Hint Resolve Pcond_Fnorm.
+
+
+(***************************************************************************
+                                                                          
+                       Main theorem                                       
+                                                                          
+  ***************************************************************************)
+
+Theorem Fnorm_FEeval_PEeval:
+ forall l fe,
+ PCond l (condition (Fnorm fe)) ->
+ FEeval l fe == NPEeval l (num (Fnorm fe)) / NPEeval l (denum (Fnorm fe)).
+Proof.
+intros l fe; elim fe; simpl.
+intros c H; rewrite CRmorph.(morph1); apply rdiv1.
+intros p H; rewrite CRmorph.(morph1); apply rdiv1.
+intros e1 He1 e2 He2 HH.
+assert (HH1: PCond l (condition (Fnorm e1))).
+apply PCond_app_inv_l with ( 1 := HH ).
+assert (HH2: PCond l (condition (Fnorm e2))).
+apply PCond_app_inv_r with ( 1 := HH ).
+rewrite (He1 HH1); rewrite (He2 HH2).
+rewrite NPEadd_correct; simpl.
+repeat rewrite NPEmul_correct; simpl.
+apply rdiv2; auto.
+
+intros e1 He1 e2 He2 HH.
+assert (HH1: PCond l (condition (Fnorm e1))).
+apply PCond_app_inv_l with ( 1 := HH ).
+assert (HH2: PCond l (condition (Fnorm e2))).
+apply PCond_app_inv_r with ( 1 := HH ).
+rewrite (He1 HH1); rewrite (He2 HH2).
+rewrite NPEsub_correct; simpl.
+repeat rewrite NPEmul_correct; simpl.
+apply rdiv3; auto.
+
+intros e1 He1 e2 He2 HH.
+assert (HH1: PCond l (condition (Fnorm e1))).
+apply PCond_app_inv_l with ( 1 := HH ).
+assert (HH2: PCond l (condition (Fnorm e2))).
+apply PCond_app_inv_r with ( 1 := HH ).
+rewrite (He1 HH1); rewrite (He2 HH2).
+repeat rewrite NPEmul_correct; simpl.
+apply rdiv4; auto.
+
+intros e1 He1 HH.
+rewrite NPEopp_correct; simpl; rewrite (He1 HH); apply rdiv5; auto.
+
+intros e1 He1 HH.
+assert (HH1: PCond l (condition (Fnorm e1))).
+apply PCond_cons_inv_r with ( 1 := HH ).
+rewrite (He1 HH1); apply rdiv6; auto.
+apply PCond_cons_inv_l with ( 1 := HH ).
+
+intros e1 He1 e2 He2 HH.
+assert (HH1: PCond l (condition (Fnorm e1))).
+apply PCond_app_inv_l with (condition (Fnorm e2)).
+apply PCond_cons_inv_r with ( 1 := HH ).
+assert (HH2: PCond l (condition (Fnorm e2))).
+apply PCond_app_inv_r with (condition (Fnorm e1)).
+apply PCond_cons_inv_r with ( 1 := HH ).
+rewrite (He1 HH1); rewrite (He2 HH2).
+repeat rewrite NPEmul_correct;simpl.
+apply rdiv7; auto.
+apply PCond_cons_inv_l with ( 1 := HH ).
+Qed.
+
+Theorem Fnorm_crossproduct:
+ forall l fe1 fe2,
+ let nfe1 := Fnorm fe1 in
+ let nfe2 := Fnorm fe2 in
+ NPEeval l (PEmul (num nfe1) (denum nfe2)) ==
+ NPEeval l (PEmul (num nfe2) (denum nfe1)) ->
+ PCond l (condition nfe1 ++ condition nfe2) ->
+ FEeval l fe1 == FEeval l fe2.
+intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
+rewrite Fnorm_FEeval_PEeval in |- *.
+ apply PCond_app_inv_l with (1 := Hcond).
+ rewrite Fnorm_FEeval_PEeval in |- *.
+  apply PCond_app_inv_r with (1 := Hcond).
+  apply cross_product_eq; trivial.
+   apply Pcond_Fnorm.
+     apply PCond_app_inv_l with (1 := Hcond).
+   apply Pcond_Fnorm.
+     apply PCond_app_inv_r with (1 := Hcond).
+Qed.
+
+(* Correctness lemmas of reflexive tactics *)
+
+Theorem Fnorm_correct:
+ forall l fe,
+ Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true ->
+ PCond l (condition (Fnorm fe)) ->  FEeval l fe == 0.
+intros l fe H H1;
+ apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1).
+apply rdiv8; auto.
+transitivity (NPEeval l (PEc cO)); auto.
+apply (ring_correct Rsth Reqe ARth CRmorph); auto.
+simpl; apply (morph0 CRmorph); auto.
+Qed.
+
+(* simplify a field expression into a fraction *)
+Theorem Pphi_dev_div_ok:
+ forall l fe nfe,
+ Fnorm fe = nfe ->
+ PCond l (condition nfe) ->
+ FEeval l fe ==
+ NPphi_dev l (Nnorm (num nfe)) / NPphi_dev l (Nnorm (denum nfe)).
+Proof.
+  intros l fe nfe eq_nfe H; subst nfe.
+  apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
+  apply SRdiv_ext;
+  apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity.
+Qed.
+
+(* solving a field equation *)
+Theorem Fnorm_correct2:
+ forall l fe1 fe2 nfe1 nfe2,
+ Fnorm fe1 = nfe1 ->
+ 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.
+apply Fnorm_crossproduct; trivial.
+apply (ring_correct Rsth Reqe ARth CRmorph); trivial.
+Qed.
+
+(* simplify a field equation : generate the crossproduct and simplify
+   polynomials *)
+Theorem Field_simplify_eq_correct :
+ forall l fe1 fe2 nfe1 nfe2,
+ Fnorm fe1 = nfe1 ->
+ Fnorm fe2 = nfe2 ->
+ NPphi_dev l (Nnorm (PEmul (num nfe1) (denum nfe2))) ==
+ NPphi_dev l (Nnorm (PEmul (num nfe2) (denum nfe1))) ->
+ PCond l (condition nfe1 ++ condition nfe2) ->
+ FEeval l fe1 == FEeval l fe2.
+Proof.
+intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond;  subst nfe1 nfe2.
+apply Fnorm_crossproduct; trivial.
+rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *.
+rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *.
+trivial.
+Qed.
+
+Section Fcons_impl.
+
+Variable Fcons : PExpr C -> list (PExpr C) -> list (PExpr C).
+
+Hypothesis PCond_fcons_inv : forall l a l1,
+  PCond l (Fcons a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
+
+Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
+  match l with
+  | nil => m
+  | cons a l1 => Fcons a (Fapp l1 m)
+  end.
+
+Lemma fcons_correct : forall l l1,
+  PCond l (Fapp l1 nil) -> PCond l l1.
+induction l1; simpl in |- *; intros.
+ trivial.
+ elim PCond_fcons_inv with (1 := H); intros.
+   destruct l1; auto.
+Qed.
+
+End Fcons_impl.
+
+Section Fcons_simpl.
+
+(* Some general simpifications of the condition: eliminate duplicates,
+   split multiplications *)
+
+Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
+ match l with
+   nil       => cons e nil
+ | cons a l1 => if PExpr_eq e a then l else cons a (Fcons e l1)
+ end.
+ 
+Theorem PFcons_fcons_inv:
+ forall l a l1, PCond l (Fcons a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
+intros l a l1; elim l1; simpl Fcons; auto.
+simpl; auto.
+intros a0 l0.
+generalize (PExpr_eq_semi_correct l a a0); case (PExpr_eq a a0).
+intros H H0 H1; split; auto.
+rewrite H; auto.
+generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
+intros H H0 H1;
+ assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
+split.
+generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
+apply H0.
+generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
+generalize Hp; case l0; simpl; intuition.
+Qed.
+
+(* equality of normal forms rather than syntactic equality *)
+Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
+ match l with
+   nil       => cons e nil
+ | cons a l1 =>
+     if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1)
+ end.
+ 
+Theorem PFcons0_fcons_inv:
+ forall l a l1, PCond l (Fcons0 a l1) ->  ~ NPEeval l a == 0 /\ PCond l l1.
+intros l a l1; elim l1; simpl Fcons0; auto.
+simpl; auto.
+intros a0 l0.
+generalize (ring_correct Rsth Reqe ARth CRmorph l a a0);
+  case (Peq ceqb (Nnorm a) (Nnorm a0)).
+intros H H0 H1; split; auto.
+rewrite H; auto.
+generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
+intros H H0 H1;
+ assert (Hp: ~ NPEeval l a0 == 0 /\ (~ NPEeval l a == 0 /\ PCond l l0)).
+split.
+generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
+apply H0.
+generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
+generalize Hp; case l0; simpl; intuition.
+Qed.
+
+Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
+ match e with
+   PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l)
+ | _ => Fcons0 e l
+ end.
+
+Theorem PFcons00_fcons_inv:
+  forall l a l1, PCond l (Fcons00 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
+intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
+ intros p H p0 H0 l1 H1.
+   simpl in H1.
+   case (H _ H1); intros H2 H3.
+   case (H0 _ H3); intros H4 H5; split; auto.
+   simpl in |- *.
+   apply field_is_integral_domain; trivial.
+Qed.
+
+
+Definition Pcond_simpl_gen := 
+  fcons_correct _ PFcons00_fcons_inv.
+
+
+(* Specific case when the equality test of coefs is complete w.r.t. the
+   field equality: non-zero coefs can be eliminated, and opposite can
+   be simplified (if -1 <> 0) *)
+
+Hypothesis ceqb_complete : forall c1 c2, phi c1 == phi c2 -> ceqb c1 c2 = true.
+
+Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
+  (phi c1 == phi c2 -> P x) ->
+  (~ phi c1 == phi c2 -> P y) ->
+  P (if ceqb c1 c2 then x else y).
+Proof.
+intros.
+generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
+generalize (ceqb_complete c1 c2).
+case (c1 ?=! c2); auto; intros.
+apply X0.
+red in |- *; intro.
+absurd (false = true); auto;  discriminate.
+Qed.
+
+Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
+ match e with
+   PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l)
+ | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l
+ | PEc c => if ceqb c cO then absurd_PCond else l
+ | _ => Fcons0 e l
+ end.
+
+Theorem PFcons1_fcons_inv:
+  forall l a l1, PCond l (Fcons1 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
+intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
+ simpl in |- *; intros c l1.
+   apply ceqb_rect_complete; intros.
+  elim (absurd_PCond_bottom l H0).
+  split; trivial.
+    rewrite <- (morph0 CRmorph) in |- *; trivial.
+ intros p H p0 H0 l1 H1.
+   simpl in H1.
+   case (H _ H1); intros H2 H3.
+   case (H0 _ H3); intros H4 H5; split; auto.
+   simpl in |- *.
+   apply field_is_integral_domain; trivial.
+ simpl in |- *; intros p H l1.
+   apply ceqb_rect_complete; intros.
+  elim (absurd_PCond_bottom l H1).
+  destruct (H _ H1).
+    split; trivial.
+    apply ropp_neq_0; trivial.
+    rewrite (morph_opp CRmorph) in H0.
+    rewrite (morph1 CRmorph) in H0.
+    rewrite (morph0 CRmorph) in H0.
+    trivial.
+Qed.
+
+Definition Fcons2 e l := Fcons1 (PExpr_simp e) l.
+ 
+Theorem PFcons2_fcons_inv:
+ forall l a l1, PCond l (Fcons2 a l1) -> ~ NPEeval l a == 0 /\ PCond l l1.
+unfold Fcons2 in |- *; intros l a l1 H; split;
+ case (PFcons1_fcons_inv l (PExpr_simp a) l1); auto.
+intros H1 H2 H3; case H1.
+transitivity (NPEeval l a); trivial.
+apply PExpr_simp_correct.
+Qed.
+
+Definition Pcond_simpl_complete := 
+  fcons_correct _ PFcons2_fcons_inv.
+
+End Fcons_simpl.
+
+End AlmostField.
+
+Section FieldAndSemiField.
+
+  Record field_theory : Prop := mk_field {
+    F_R : ring_theory rO rI radd rmul rsub ropp req;
+    F_1_neq_0 : ~ 1 == 0;
+    Fdiv_def : forall p q, p / q == p * / q;
+    Finv_l : forall p, ~ p == 0 ->  / p * p == 1
+  }.
+
+  Definition F2AF f :=
+    mk_afield
+      (Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l).
+
+  Record semi_field_theory : Prop := mk_sfield {
+    SF_SR : semi_ring_theory rO rI radd rmul req;
+    SF_1_neq_0 : ~ 1 == 0;
+    SFdiv_def : forall p q, p / q == p * / q;
+    SFinv_l : forall p, ~ p == 0 ->  / p * p == 1
+  }.
+
+End FieldAndSemiField.
+
+End MakeFieldPol.
+
+  Definition SF2AF R rO rI radd rmul rdiv rinv req Rsth 
+    (sf:semi_field_theory R rO rI radd rmul rdiv rinv req)  :=
+    mk_afield _ _ _ _ _ _ _ _ _ _
+      (SRth_ARth Rsth sf.(SF_SR _ _ _ _ _ _ _ _))
+      sf.(SF_1_neq_0 _ _ _ _ _ _ _ _)
+      sf.(SFdiv_def _ _ _ _ _ _ _ _)
+      sf.(SFinv_l _ _ _ _ _ _ _ _).
+
+
+Section Complete.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable (rdiv : R -> R ->  R) (rinv : 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 " := (rdiv x y).  Notation "/ x" := (rinv x).
+  Notation "x == y" := (req x y) (at level 70, no associativity).
+ Variable Rsth : Setoid_Theory R req.
+   Add Setoid R req Rsth as R_setoid3.
+ Variable Reqe : ring_eq_ext radd rmul ropp req.
+   Add Morphism radd : radd_ext3.  exact (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext3.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext3.  exact (Ropp_ext Reqe). Qed.
+
+Section AlmostField.
+
+ Variable AFth : almost_field_theory R rO rI radd rmul rsub ropp rdiv rinv req.
+ Let ARth := AFth.(AF_AR _ _ _ _ _ _ _ _ _ _).
+ Let rI_neq_rO := AFth.(AF_1_neq_0 _ _ _ _ _ _ _ _ _ _).
+ Let rdiv_def := AFth.(AFdiv_def _ _ _ _ _ _ _ _ _ _).
+ Let rinv_l := AFth.(AFinv_l _ _ _ _ _ _ _ _ _ _).
+
+Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
+
+Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
+
+Lemma add_inj_r : forall p x y,
+   gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
+intros p x y.
+elim p using Pind; simpl in |- *; intros.
+ apply S_inj; trivial.
+ apply H.
+   apply S_inj.
+   repeat rewrite (ARadd_assoc ARth) in |- *.
+   rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial.
+Qed.
+
+Lemma gen_phiPOS_inj : forall x y,
+  gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
+  x = y.
+intros x y.
+repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
+ElimPcompare x y; intro.
+ intros.
+   apply Pcompare_Eq_eq; trivial.
+ intro.
+   elim gen_phiPOS_not_0 with (y - x)%positive.
+   apply add_inj_r with x.
+   symmetry  in |- *.
+   rewrite (ARadd_0_r Rsth ARth) in |- *.
+   rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+   rewrite Pplus_minus in |- *; trivial.
+   change Eq with (CompOpp Eq) in |- *.
+   rewrite <- Pcompare_antisym in |- *; trivial.
+   rewrite H in |- *; trivial.
+ intro.
+   elim gen_phiPOS_not_0 with (x - y)%positive.
+   apply add_inj_r with y.
+   rewrite (ARadd_0_r Rsth ARth) in |- *.
+   rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+   rewrite Pplus_minus in |- *; trivial.
+Qed.
+
+
+Lemma gen_phiN_inj : forall x y,
+  gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
+  x = y.
+destruct x; destruct y; simpl in |- *; intros; trivial.
+ elim gen_phiPOS_not_0 with p.
+   symmetry  in |- *.
+   rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
+ rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial.
+Qed.
+
+Lemma gen_phiN_complete : forall x y,
+  gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
+  Neq_bool x y = true.
+intros.
+ replace y with x.
+ unfold Neq_bool in |- *.
+   rewrite Ncompare_refl in |- *; trivial.
+ apply gen_phiN_inj; trivial.
+Qed.
+
+End AlmostField.
+
+Section Field.
+
+ Variable Fth : field_theory R rO rI radd rmul rsub ropp rdiv rinv req.
+ Let Rth := Fth.(F_R _ _ _ _ _ _ _ _ _ _).
+ Let rI_neq_rO := Fth.(F_1_neq_0 _ _ _ _ _ _ _ _ _ _).
+ Let rdiv_def := Fth.(Fdiv_def _ _ _ _ _ _ _ _ _ _).
+ Let rinv_l := Fth.(Finv_l _ _ _ _ _ _ _ _ _ _).
+ Let AFth := F2AF _ _ _ _ _ _ _ _ _ _ Rsth Reqe Fth.
+ Let ARth := Rth_ARth Rsth Reqe Rth.
+
+Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
+intros.
+transitivity (x + (1 + - (1))).
+ rewrite (Ropp_def Rth) in |- *.
+   symmetry  in |- *.
+   apply (ARadd_0_r Rsth ARth).
+ transitivity (y + (1 + - (1))).
+  repeat rewrite <- (ARplus_assoc ARth) in |- *.
+    repeat rewrite (ARadd_assoc ARth) in |- *.
+    apply (Radd_ext Reqe).
+   repeat rewrite <- (ARadd_sym ARth 1) in |- *.
+     trivial.
+   reflexivity.
+  rewrite (Ropp_def Rth) in |- *.
+    apply (ARadd_0_r Rsth ARth).
+Qed.
+
+
+ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
+
+Let gen_phiPOS_inject :=
+   gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
+
+Lemma gen_phiPOS_discr_sgn : forall x y,
+  ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
+red in |- *; intros.
+apply gen_phiPOS_not_0 with (y + x)%positive.
+rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
+ apply (Radd_ext Reqe); trivial.
+  reflexivity.
+  rewrite (same_gen Rsth Reqe ARth) in |- *.
+    rewrite (same_gen Rsth Reqe ARth) in |- *.
+    trivial.
+ apply (Ropp_def Rth).
+Qed.
+
+Lemma gen_phiZ_inj : forall x y,
+  gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
+  x = y.
+destruct x; destruct y; simpl in |- *; intros.
+ trivial.
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   symmetry  in |- *; trivial.
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
+   rewrite <- H in |- *.
+   apply (ARopp_zero Rsth Reqe ARth).
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   trivial.
+ rewrite gen_phiPOS_inject  with (1 := H) in |- *; trivial.
+ elim gen_phiPOS_discr_sgn with (1 := H).
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
+   rewrite H in |- *.
+   apply (ARopp_zero Rsth Reqe ARth).
+ elim gen_phiPOS_discr_sgn with p0 p.
+   symmetry  in |- *; trivial.
+ replace p0 with p; trivial.
+   apply gen_phiPOS_inject.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *.
+   rewrite H in |- *; trivial.
+   reflexivity.
+Qed.
+
+Lemma gen_phiZ_complete : forall x y,
+  gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
+  Zeq_bool x y = true.
+intros.
+ replace y with x.
+ unfold Zeq_bool in |- *.
+   rewrite Zcompare_refl in |- *; trivial.
+ apply gen_phiZ_inj; trivial.
+Qed.
+
+End Field.
+
+End Complete.
+
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
new file mode 100644
index 000000000..2ac96b826
--- /dev/null
+++ b/contrib/setoid_ring/Field_tac.v
@@ -0,0 +1,161 @@
+(************************************************************************)
+(*  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 Ring_tac.
+Require Import InitialRing.
+Require Import Field.
+
+ (* syntaxification *)
+ Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv := 
+ let rec mkP t :=
+    match Cst t with
+    | Ring_tac.NotConstant =>
+        match t with 
+        | (radd ?t1 ?t2) => 
+          let e1 := mkP t1 in
+          let e2 := mkP t2 in constr:(FEadd C e1 e2)
+        | (rmul ?t1 ?t2) => 
+          let e1 := mkP t1 in
+          let e2 := mkP t2 in constr:(FEmul C e1 e2)
+        | (rsub ?t1 ?t2) => 
+          let e1 := mkP t1 in
+          let e2 := mkP t2 in constr:(FEsub C e1 e2)
+        | (ropp ?t1) =>
+          let e1 := mkP t1 in constr:(FEopp C e1)
+        | (rdiv ?t1 ?t2) => 
+          let e1 := mkP t1 in
+          let e2 := mkP t2 in constr:(FEdiv C e1 e2)
+        | (rinv ?t1) =>
+          let e1 := mkP t1 in constr:(FEinv C e1)
+        | _ =>
+          let p := Find_at t fv in constr:(FEX C p)
+        end
+    | ?c => constr:(FEc C c)
+    end
+ in mkP t.
+
+Ltac FFV Cst add mul sub opp div inv t fv :=
+ let rec TFV t fv :=
+  match Cst t with
+  | Ring_tac.NotConstant =>
+      match t with
+      | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
+      | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
+      | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
+      | (opp ?t1) => TFV t1 fv
+      | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
+      | (inv ?t1) => TFV t1 fv
+      | _ => AddFvTail t fv
+      end
+  | _ => fv
+  end 
+ in TFV t fv.
+
+(* simplifying the non-zero condition... *)
+
+Ltac fold_field_cond req rO :=
+  let rec fold_concl t :=
+    match t with
+      ?x /\ ?y =>
+        let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy)
+    | req ?x rO -> False => constr:(~ req x rO)
+    | _ => t
+    end in
+  match goal with
+    |- ?t => let ft := fold_concl t in change ft
+  end.
+
+Ltac simpl_PCond req rO :=
+  protect_fv "field";
+  try (exact I);
+  fold_field_cond req rO.
+
+(* Rewriting *)
+Ltac Field_rewrite_list lemma Cond_lemma req Cst_tac :=
+  let Make_tac :=
+    match type of lemma with
+    | forall l fe nfe,
+      _ = nfe -> 
+      PCond _ _ _ _ _ _ _ _ _ _ _ ->
+      req (FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi l fe) _ =>
+        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_field H := (*protect_fv "field" in H*)
+unfold Pphi_dev in H;simpl in H in 
+        (fun f => f mkFV mkFE simpl_field lemma req;
+                  try (apply Cond_lemma; simpl_PCond req rO))
+    | _ => fail 1 "field anomaly: bad correctness lemma"
+    end in
+  Make_tac ReflexiveRewriteTactic.
+(* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
+
+
+(* Generic form of field tactics *)
+Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
+  let ParseLemma :=
+    match type of lemma with
+    | forall l fe1 fe2 nfe1 nfe2, _ = nfe1 -> _ = nfe2 -> _ -> 
+      PCond _ _ _ _ _ _ _ _ _ _ _ ->
+      req (FEeval ?R ?rO _ _ _ _ _ _ _ _ l fe1) _ =>
+        (fun f => f R rO)
+    | _ => fail 1 "field anomaly: bad correctness lemma" 
+    end in
+  let ParseExpr2 ilemma :=
+    match type of ilemma with
+      forall nfe1 nfe2, ?fe1 = nfe1 -> ?fe2 = nfe2 -> _ => (fun f => f fe1 fe2)
+    | _ => fail 1 "field anomaly: cannot find norm expression"
+    end in
+  let Main r1 r2 R rO :=
+    let fv := FV_tac r1 (@List.nil R) in
+    let fv := FV_tac r2 fv in
+    let fe1 := SYN_tac r1 fv in
+    let fe2 := SYN_tac r2 fv in
+    let nfrac1 := fresh "frac1" in 
+    let norm_hyp1 := fresh "norm_frac1" in
+    let nfrac2 := fresh "frac2" in 
+    let norm_hyp2 := fresh "norm_frac2" in
+    ParseExpr2 (lemma fv fe1 fe2)
+    ltac:(fun nfrac_val1 nfrac_val2 =>
+          (compute_assertion norm_hyp1 nfrac1 nfrac_val1;
+           compute_assertion norm_hyp2 nfrac2 nfrac_val2;
+           (apply (lemma fv fe1 fe2 nfrac1 nfrac2 norm_hyp1 norm_hyp2)
+            || fail "field anomaly: failed in applying lemma");
+           [ SIMPL_tac | apply Cond_lemma; simpl_PCond req rO];
+           try clear nfrac1 nfrac2 norm_hyp1 norm_hyp2)) in
+  ParseLemma ltac:(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: bad correctness lemma"
+  end.
+
+(* solve completely a field equation, leaving non-zero conditions to be
+   proved *)
+Ltac Make_field_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 :=
+      vm_compute; (reflexivity || fail "not a valid field equation") in
+    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
+  ParseFieldComponents lemma req Main.
+
+(* transforms a field equation to an equivalent (simplified) ring equation,
+   and leaves non-zero conditions to be proved *)
+Ltac Make_field_simplify_eq_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 := (unfold Pphi_dev; simpl) in
+    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
+  ParseFieldComponents lemma req Main.
diff --git a/contrib/setoid_ring/ZRing_th.v b/contrib/setoid_ring/InitialRing.v
index 08eb54aa8..19ffe1d53 100644
--- a/contrib/setoid_ring/ZRing_th.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -11,7 +11,7 @@ Require Import BinInt.
 Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_base.
-Require Import Pol.
+Require Import Ring_polynom.
 Set Implicit Arguments.
 
 Import RingSyntax.
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
new file mode 100644
index 000000000..e322d9e21
--- /dev/null
+++ b/contrib/setoid_ring/NArithRing.v
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  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 NArith.
+Require Export Ring.
+Set Implicit Arguments.
+
+Ltac isNcst t :=
+  let t := eval hnf in t in
+  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 Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).
diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
new file mode 100644
index 000000000..8793e3622
--- /dev/null
+++ b/contrib/setoid_ring/RealField.v
@@ -0,0 +1,573 @@
+Require Import Ring_polynom InitialRing Field Field_tac Ring.
+
+Require Export Rdefinitions.
+Require Export Raxioms.
+Require Export RIneq.
+
+Section RField.
+
+Notation NPEeval := (PEeval 0%R Rplus Rmult Rminus Ropp
+   (gen_phiZ 0%R 1%R Rplus Rmult Ropp)).
+Notation NPCond :=
+ (PCond _ 0%R Rplus Rmult Rminus Ropp (@eq R) _
+   (gen_phiZ 0%R 1%R Rplus Rmult Ropp)).
+(*
+Lemma RTheory : ring_theory 0%R 1%R Rplus Rmult Rminus Ropp (eq (A:=R)).
+Proof.
+constructor.
+ intro; apply Rplus_0_l.
+ exact Rplus_comm.
+ symmetry  in |- *; apply Rplus_assoc.
+ intro; apply Rmult_1_l.
+ exact Rmult_comm.
+ symmetry  in |- *; apply Rmult_assoc.
+ intros m n p.
+   rewrite Rmult_comm in |- *.
+   rewrite (Rmult_comm n p) in |- *.
+   rewrite (Rmult_comm m p) in |- *.
+   apply Rmult_plus_distr_l.
+ reflexivity.
+ exact Rplus_opp_r.
+Qed.
+Add Ring Rring : RTheory Abstract.
+*)
+Notation Rset := (Eqsth R).
+Notation Rext := (Eq_ext Rplus Rmult Ropp).
+Notation Rmorph := (gen_phiZ_morph Rset Rext RTheory).
+
+(*
+Adds Field RF : Rfield Abstract.
+*)
+
+Lemma Rlt_n_Sn : forall x, (x < x + 1)%R.
+Proof.
+intro.
+elim archimed with x; intros.
+destruct H0.
+ apply Rlt_trans with (IZR (up x)); trivial.
+    replace (IZR (up x)) with (x + (IZR (up x) - x))%R.
+  apply Rplus_lt_compat_l; trivial.
+  unfold Rminus in |- *.
+    rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
+    rewrite <- Rplus_assoc in |- *.
+    rewrite Rplus_opp_r in |- *.
+    apply Rplus_0_l.
+ elim H0.
+   unfold Rminus in |- *.
+   rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
+   rewrite <- Rplus_assoc in |- *.
+   rewrite Rplus_opp_r in |- *.
+   rewrite Rplus_0_l in |- *; trivial.
+Qed.
+
+
+(*
+Lemma Rdiscr_0_2 : (2 <> 0)%R.
+red in |- *; intro.
+assert (0 < 1)%R.
+ elim (archimed 0); intros.
+   unfold Rminus in H1.
+   rewrite (ARopp_zero Rset Rext (Rth_ARth Rset Rext RTheory)) in H1.
+   rewrite (ARadd_0_r Rset (Rth_ARth Rset Rext RTheory)) in H1.
+   destruct H1.
+  apply Rlt_trans with (IZR (up 0)); trivial.
+  elim H1; trivial.
+ assert (1 < 2)%R.
+  pattern 1%R at 1 in |- *.
+     replace 1%R with (1 + 0)%R.
+   apply Rplus_lt_compat_l.
+     trivial.
+   rewrite (ARadd_0_r Rset (Rth_ARth Rset Rext RTheory)) in |- *.
+     trivial.
+  apply (Rlt_asym 0 1); trivial.
+    elim H; trivial.
+Qed.
+*)
+
+Lemma Rgen_phiPOS : forall x, (gen_phiPOS1 1 Rplus Rmult x > 0)%R.
+unfold Rgt in |- *.
+induction x; simpl in |- *; intros.
+ apply Rlt_trans with (1 + 0)%R.
+  rewrite Rplus_comm in |- *.
+    apply Rlt_n_Sn.
+  apply Rplus_lt_compat_l.
+    rewrite <- (Rmul_0_l Rset Rext RTheory 2%R) in |- *.
+    rewrite Rmult_comm in |- *.
+    apply Rmult_lt_compat_l.
+   apply Rlt_trans with (0 + 1)%R.
+    apply Rlt_n_Sn.
+    rewrite Rplus_comm in |- *.
+      apply Rplus_lt_compat_l.
+       replace 1%R with (0 + 1)%R; auto with real.
+   trivial.
+ rewrite <- (Rmul_0_l Rset Rext RTheory 2%R) in |- *.
+   rewrite Rmult_comm in |- *.
+   apply Rmult_lt_compat_l.
+  apply Rlt_trans with (0 + 1)%R.
+   apply Rlt_n_Sn.
+   rewrite Rplus_comm in |- *.
+     apply Rplus_lt_compat_l.
+      replace 1%R with (0 + 1)%R; auto with real.
+  trivial.
+ auto with real.
+Qed.
+(*
+unfold Rgt in |- *.
+induction x; simpl in |- *; intros.
+ apply Rplus_lt_0_compat; auto with real.
+   apply Rmult_lt_0_compat; auto with real.
+ apply Rmult_lt_0_compat; auto with real.
+ auto with real.
+*)
+
+Lemma Rgen_phiPOS_not_0 : forall x, (gen_phiPOS1 1 Rplus Rmult x <> 0)%R.
+red in |- *; intros.
+specialize (Rgen_phiPOS x).
+rewrite H in |- *; intro.
+apply (Rlt_asym 0 0); trivial.
+Qed.
+
+
+
+Let ARfield :=
+  F2AF _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield.
+
+(*Let Rring := AF_AR _ _ _ _ _ _ _ _ _ _ ARfield.*)
+
+Notation NPFcons_inv :=
+  (PFcons_fcons_inv
+    _ _ _ _ _ _ _ _ Rset Rext ARfield _ _ _ _ _ _ _ _ _ Rmorph).
+
+
+(*
+Theorem SRinv_ext: forall p q:R, p=q -> (/p = /q)%R.
+intros p q; apply f_equal with ( f := Rinv ); auto.
+Qed.
+
+Add Morphism Rinv : Rinv_morph.
+Proof.
+exact SRinv_ext.
+Qed.
+*)
+Notation Rphi := (gen_phiZ 0%R 1%R Rplus Rmult Ropp).
+
+Theorem gen_phiPOS1_IZR :
+ forall p, gen_phiPOS 1%R Rplus Rmult p = IZR (Zpos p).
+intros p; elim p; simpl gen_phiPOS.
+intros p0; case p0.
+intros p1 H; rewrite H.
+unfold IZR; rewrite (nat_of_P_xI (xI p1)); (try rewrite S_INR);
+ (try rewrite plus_INR); (try rewrite mult_INR).
+pose (x:= INR (nat_of_P (xI p1))); fold x; simpl; ring.
+intros p1 H; rewrite H.
+unfold IZR; rewrite (nat_of_P_xI (xO p1)); (try rewrite S_INR);
+ (try rewrite plus_INR); (try rewrite mult_INR).
+pose (x:= INR (nat_of_P (xO p1))); fold x; simpl; ring.
+simpl; intros; ring.
+intros p0; case p0.
+intros p1 H; rewrite H.
+unfold IZR; rewrite (nat_of_P_xO (xI p1)); (try rewrite S_INR);
+ (try rewrite plus_INR); (try rewrite mult_INR).
+pose (x:= INR (nat_of_P (xO p1))); fold x; simpl; ring.
+intros p1 H; rewrite H.
+unfold IZR; rewrite (nat_of_P_xO (xO p1)); (try rewrite S_INR);
+ (try rewrite plus_INR); (try rewrite mult_INR).
+pose (x:= INR (nat_of_P (xO p1))); fold x; simpl; ring.
+simpl; intros; ring.
+simpl; trivial.
+Qed.
+ 
+Theorem gen_phiZ1_IZR: forall p, Rphi p = IZR p.
+intros p; case p; simpl; auto.
+intros p0; rewrite gen_phiPOS1_IZR; auto.
+intros p0; rewrite gen_phiPOS1_IZR; auto.
+Qed.
+
+Lemma Zeq_bool_complete : forall x y, Rphi x = Rphi y -> Zeq_bool x y = true.
+Proof.
+intros.
+ replace y with x.
+ unfold Zeq_bool in |- *.
+   rewrite Zcompare_refl in |- *; trivial.
+ assert (IZR x = IZR y); auto.
+  repeat rewrite <- gen_phiZ1_IZR in |- *; trivial.
+  apply eq_IZR; trivial.
+Qed.
+
+
+Section Complete.
+Import Setoid.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable (rdiv : R -> R ->  R) (rinv : 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 " := (rdiv x y).  Notation "/ x" := (rinv x).
+  Notation "x == y" := (req x y) (at level 70, no associativity).
+  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 (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext3.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext3.  exact (Ropp_ext Reqe). Qed.
+
+Section AlmostField.
+
+ Variable AFth : almost_field_theory R rO rI radd rmul rsub ropp rdiv rinv req.
+ Let ARth := AFth.(AF_AR _ _ _ _ _ _ _ _ _ _).
+ Let rI_neq_rO := AFth.(AF_1_neq_0 _ _ _ _ _ _ _ _ _ _).
+ Let rdiv_def := AFth.(AFdiv_def _ _ _ _ _ _ _ _ _ _).
+ Let rinv_l := AFth.(AFinv_l _ _ _ _ _ _ _ _ _ _).
+
+Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
+
+Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
+
+Lemma discr_0_2 : ~ 1+1 == 0.
+change (~ gen_phiPOS 1 radd rmul 2 == 0) in |- *.
+rewrite <- (same_gen Rsth Reqe ARth) in |- *.
+apply gen_phiPOS_not_0.
+Qed.
+Hint Resolve discr_0_2.
+
+
+Lemma double_inj : forall x y, (1+1)*x==(1+1)*y -> x==y.
+intros.
+assert (/ (1 + 1) * ((1 + 1) * x) == / (1 + 1) * ((1 + 1) * y)).
+ rewrite H in |- *; trivial.
+   reflexivity.
+ generalize H0; clear H0.
+   repeat rewrite (ARmul_assoc ARth) in |- *.
+   repeat rewrite (AFinv_l _ _ _ _ _ _ _ _ _ _ AFth) in |- *; trivial.
+   repeat rewrite (ARmul_1_l ARth) in |- *; trivial.
+Qed.
+
+Lemma discr_even_1 : forall x,
+  ~ (1+1) * gen_phiPOS1 rI radd rmul x == 1.
+intros.
+rewrite (same_gen Rsth Reqe ARth) in |- *.
+elim x using Pcase; simpl in |- *; intros.
+ rewrite (ARmul_1_r Rsth ARth) in |- *.
+   red in |- *; intro.
+   apply rI_neq_rO.
+   apply S_inj.
+   rewrite H in |- *.
+   rewrite (ARadd_0_r Rsth ARth) in |- *; reflexivity.
+ rewrite <- (same_gen Rsth Reqe ARth) in |- *.
+   rewrite (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *.
+   rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+   rewrite (ARmul_1_r Rsth ARth) in |- *.
+   red in |- *; intro.
+   apply (gen_phiPOS_not_0 (xI n)).
+   apply S_inj; simpl in |- *.
+   rewrite (ARadd_assoc ARth) in |- *.
+   rewrite H in |- *.
+   rewrite (ARadd_0_r Rsth ARth) in |- *; reflexivity.
+Qed.
+
+Lemma discr_odd_0 : forall x,
+  ~ 1 + (1+1) * gen_phiPOS1 rI radd rmul x == 0.
+red in |- *; intros.
+apply discr_even_1 with (Psucc x).
+rewrite (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *.
+rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+rewrite (ARmul_1_r Rsth ARth) in |- *.
+rewrite <- (ARadd_assoc ARth) in |- *.
+rewrite H in |- *.
+apply (ARadd_0_r Rsth ARth).
+Qed.
+
+
+Lemma add_inj_r : forall p x y,
+   gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
+intros p x y.
+elim p using Pind; simpl in |- *; intros.
+ apply S_inj; trivial.
+ apply H.
+   apply S_inj.
+   repeat rewrite (ARadd_assoc ARth) in |- *.
+   rewrite <- (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *; trivial.
+Qed.
+
+Lemma discr_0_1: ~ 1 == 0.
+red in |- *; intro.
+apply (discr_even_1 1).
+simpl in |- *.
+rewrite H in |- *.
+apply (ARmul_0_r Rsth ARth).
+Qed.
+
+
+Lemma discr_diag : forall x,
+  ~ 1 + gen_phiPOS1 rI radd rmul x == gen_phiPOS1 rI radd rmul x.
+intro.
+elim x using Pind; simpl in |- *; intros.
+ red in |- *; intro; apply discr_0_1.
+   apply S_inj.
+   rewrite (ARadd_0_r Rsth ARth) in |- *.
+   trivial.
+ rewrite (ARgen_phiPOS_Psucc Rsth Reqe ARth) in |- *.
+   red in |- *; intro; apply H.
+   apply S_inj; trivial.
+Qed.
+
+Lemma even_odd_discr : forall x y,
+  ~ 1 + (1+1) * gen_phiPOS1 rI radd rmul x == 
+   (1+1) * gen_phiPOS1 rI radd rmul y.
+intros.
+ElimPcompare x y; intro.
+  replace y with x.
+  apply (discr_diag (xO x)).
+  apply Pcompare_Eq_eq; trivial.
+  replace y with (x + (y - x))%positive.
+  rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+    rewrite (ARadd_sym ARth) in |- *.
+    rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+    red in |- *; intros.
+    apply discr_even_1 with (y - x)%positive.
+    symmetry  in |- *.
+    apply add_inj_r with (xO x); trivial.
+  apply Pplus_minus.
+    change Eq with (CompOpp Eq) in |- *.
+    rewrite <- Pcompare_antisym in |- *; trivial.
+    simpl in |- *.
+    rewrite H in |- *; trivial.
+  replace x with (y + (x - y))%positive.
+  rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+    rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+    rewrite (ARadd_assoc ARth) in |- *.
+    red in |- *; intro.
+    apply discr_odd_0 with (x - y)%positive.
+    apply add_inj_r with (xO y).
+    simpl in |- *.
+    rewrite (ARadd_0_r Rsth ARth) in |- *.
+    rewrite (ARadd_assoc ARth) in |- *.
+    rewrite (ARadd_sym ARth ((1 + 1) * gen_phiPOS1 1 radd rmul y)) in |- *.
+    trivial.
+  apply Pplus_minus; trivial.
+Qed.
+
+(* unused fact *)
+Lemma even_0_inv : forall x, (1+1) * x == 0 -> x == 0.
+Proof.
+intros.
+apply double_inj.
+rewrite (ARmul_0_r Rsth ARth) in |- *.
+trivial.
+Qed.
+
+Lemma gen_phiPOS_inj : forall x y,
+  gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
+  x = y.
+intros x y.
+repeat rewrite <- (same_gen Rsth Reqe ARth) in |- *.
+generalize y; clear y.
+induction x; destruct y; simpl in |- *; intros.
+  replace y with x; trivial.
+   apply IHx.
+   apply double_inj; apply S_inj; trivial.
+ elim even_odd_discr with (1 := H).
+ elim gen_phiPOS_not_0 with (xO x).
+   apply S_inj.
+   rewrite (ARadd_0_r Rsth ARth) in |- *.
+   trivial.
+ elim even_odd_discr with y x.
+   symmetry  in |- *.
+   trivial.
+  replace y with x; trivial.
+   apply IHx.
+   apply double_inj; trivial.
+ elim discr_even_1 with x.
+   trivial.
+ elim gen_phiPOS_not_0 with (xO y).
+   apply S_inj.
+   rewrite (ARadd_0_r Rsth ARth) in |- *.
+   symmetry  in |- *; trivial.
+ elim discr_even_1 with y.
+   symmetry  in |- *; trivial.
+ trivial.
+Qed.
+
+
+Lemma gen_phiN_inj : forall x y,
+  gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
+  x = y.
+destruct x; destruct y; simpl in |- *; intros; trivial.
+ elim gen_phiPOS_not_0 with p.
+   symmetry  in |- *.
+   rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *; trivial.
+ rewrite gen_phiPOS_inj with (1 := H) in |- *; trivial.
+Qed.
+
+End AlmostField.
+
+Section Field.
+
+ Variable Fth : field_theory R rO rI radd rmul rsub ropp rdiv rinv req.
+ Let Rth := Fth.(F_R _ _ _ _ _ _ _ _ _ _).
+ Let rI_neq_rO := Fth.(F_1_neq_0 _ _ _ _ _ _ _ _ _ _).
+ Let rdiv_def := Fth.(Fdiv_def _ _ _ _ _ _ _ _ _ _).
+ Let rinv_l := Fth.(Finv_l _ _ _ _ _ _ _ _ _ _).
+ Let AFth := F2AF _ _ _ _ _ _ _ _ _ _ Rsth Reqe Fth.
+ Let ARth := Rth_ARth Rsth Reqe Rth.
+
+Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
+intros.
+transitivity (x + (1 + - (1))).
+ rewrite (Ropp_def Rth) in |- *.
+   symmetry  in |- *.
+   apply (ARadd_0_r Rsth ARth).
+ transitivity (y + (1 + - (1))).
+  repeat rewrite <- (ARplus_assoc ARth) in |- *.
+    repeat rewrite (ARadd_assoc ARth) in |- *.
+    apply (Radd_ext Reqe).
+   repeat rewrite <- (ARadd_sym ARth 1) in |- *.
+     trivial.
+   reflexivity.
+  rewrite (Ropp_def Rth) in |- *.
+    apply (ARadd_0_r Rsth ARth).
+Qed.
+
+
+ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
+
+Let gen_phiPOS_inject :=
+   gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
+
+Lemma gen_phiPOS_discr_sgn : forall x y,
+  ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
+red in |- *; intros.
+apply gen_phiPOS_not_0 with (y + x)%positive.
+rewrite (ARgen_phiPOS_add Rsth Reqe ARth) in |- *.
+transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y).
+ apply (Radd_ext Reqe); trivial.
+  reflexivity.
+  rewrite (same_gen Rsth Reqe ARth) in |- *.
+    rewrite (same_gen Rsth Reqe ARth) in |- *.
+    trivial.
+ apply (Ropp_def Rth).
+Qed.
+
+Lemma gen_phiZ_inj : forall x y,
+  gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
+  x = y.
+destruct x; destruct y; simpl in |- *; intros.
+ trivial.
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   symmetry  in |- *; trivial.
+ elim gen_phiPOS_not_0 with p.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS1 1 radd rmul p)) in |- *.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   rewrite <- H in |- *.
+   apply (ARopp_zero Rsth Reqe ARth).
+ elim gen_phiPOS_not_0 with p.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   trivial.
+ rewrite gen_phiPOS_inject  with (1 := H) in |- *; trivial.
+ elim gen_phiPOS_discr_sgn with (1 := H).
+ elim gen_phiPOS_not_0 with p.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS1 1 radd rmul p)) in |- *.
+   rewrite (same_gen Rsth Reqe ARth) in |- *.
+   rewrite H in |- *.
+   apply (ARopp_zero Rsth Reqe ARth).
+ elim gen_phiPOS_discr_sgn with p0 p.
+   symmetry  in |- *; trivial.
+  replace p0 with p; trivial.
+   apply gen_phiPOS_inject.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)) in |- *.
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)) in |- *.
+   rewrite H in |- *; trivial.
+   reflexivity.
+Qed.
+
+Lemma gen_phiZ_complete : forall x y,
+  gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
+  Zeq_bool x y = true.
+intros.
+ replace y with x.
+ unfold Zeq_bool in |- *.
+   rewrite Zcompare_refl in |- *; trivial.
+ apply gen_phiZ_inj; trivial.
+Qed.
+
+End Field.
+
+End Complete.
+
+
+
+
+
+(*
+Definition Rlemma1 :=
+  (Pphi_dev_div_ok_compl _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield
+    _ _ _ _ _ _ _ _ _ Rmorph Zeq_bool_complete).
+
+Definition Rlemma2 :=
+  (Fnorm_correct_gen _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield
+    _ _ _ _ _ _ _ _ _ Rmorph).
+
+Definition Rlemma2' :=
+  (Fnorm_correct_compl _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield
+    _ _ _ _ _ _ _ _ _ Rmorph Zeq_bool_complete).
+
+Definition Rlemma3 :=
+  (Field_simplify_eq_correct_compl
+    _ _ _ _ _ _ _ _ _ _ Rset Rext SRinv_ext ARfield
+    _ _ _ _ _ _ _ _ _ Rmorph Zeq_bool_complete).
+
+Notation Fcons := (Fcons2 Z 0%Z Zplus Zmult Zminus Zopp Zeq_bool).
+*)
+
+End RField.
+(*
+Ltac newfield :=
+  Make_field_tac
+    Rlemma2' (eq (A:=R)) ltac:(inv_gen_phiZ 0%R 1%R Rplus Rmult Ropp).
+
+Section Compat.
+Open Scope R_scope.
+
+(** Inverse *)
+Lemma Rinv_1 : / 1 = 1.
+newfield; auto with real.
+Qed.
+
+(*********)
+Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r.
+intros; newfield; auto with real.
+Qed.
+
+(*********)
+Lemma Rinv_mult_distr :
+ forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2.
+intros; newfield; auto with real.
+Qed.
+
+(*********)
+Lemma Ropp_inv_permute : forall r, r <> 0 -> - / r = / - r.
+intros; newfield; auto with real.
+Qed.
+End Compat.
+
+Ltac field := newfield.
+Ltac field_simplify_eq :=
+   Make_field_simplify_eq_tac
+     Rlemma3 (eq (A:=R)) ltac:(inv_gen_phiZ 0%R 1%R Rplus Rmult Ropp).
+Ltac field_simplify :=
+   Field_rewrite_list
+     Rlemma1 (eq (A:=R)) ltac:(inv_gen_phiZ 0%R 1%R Rplus Rmult Ropp).
+*)
+(*
+Ltac newfield_rewrite r :=
+  let T := Rfield.Make_field_rewrite in
+  T Rplus Rmult Rminus Ropp Rinv Rdiv Fcons2 PFcons2_fcons_inv RCst r;
+  unfold_field.
+*)
+
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index 45f59a557..72571c72e 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -7,9 +7,9 @@
 (************************************************************************)
 
 Require Import Bool.
-Require Export Ring_th.
+Require Export Ring_theory.
 Require Export Ring_base.
-Require Import ZRing_th.
+Require Import InitialRing.
 Require Import Ring_equiv.
 
 Lemma BoolTheory :
diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v
index 2209f0643..e0ff5b023 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/contrib/setoid_ring/Ring_base.v
@@ -11,5 +11,5 @@
    ZArith_base. *)
 
 Declare ML Module "newring".
-Require Export Ring_th.
+Require Export Ring_theory.
 Require Export Ring_tac.
diff --git a/contrib/setoid_ring/Ring_equiv.v b/contrib/setoid_ring/Ring_equiv.v
index 135a59e01..945f6c684 100644
--- a/contrib/setoid_ring/Ring_equiv.v
+++ b/contrib/setoid_ring/Ring_equiv.v
@@ -1,6 +1,6 @@
+Require Import Setoid_ring_theory.
+Require Import LegacyRing_theory.
 Require Import Ring_theory.
-Require Import Coq.ring.Setoid_ring_theory.
-Require Import Ring_th.
 
 Set Implicit Arguments.
 
diff --git a/contrib/setoid_ring/Pol.v b/contrib/setoid_ring/Ring_polynom.v
index ff5608b8a..a06991c7e 100644
--- a/contrib/setoid_ring/Pol.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -11,7 +11,7 @@ Require Import Setoid.
 Require Export BinList.
 Require Import BinPos.
 Require Import BinInt.
-Require Export Ring_th.
+Require Export Ring_theory.
 
 Import RingSyntax.
 
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index a6ac66881..bfb83fbe0 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -1,7 +1,7 @@
 Set Implicit Arguments.
 Require Import Setoid.
 Require Import BinPos.
-Require Import Pol.
+Require Import Ring_polynom.
 Require Import BinList.
 Declare ML Module "newring".
 
diff --git a/contrib/setoid_ring/Ring_th.v b/contrib/setoid_ring/Ring_theory.v
index a7dacaa75..a7dacaa75 100644
--- a/contrib/setoid_ring/Ring_th.v
+++ b/contrib/setoid_ring/Ring_theory.v
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
new file mode 100644
index 000000000..4dbc725b8
--- /dev/null
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  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 Export Ring.
+Require Import ZArith_base.
+Import InitialRing.
+Set Implicit Arguments.
+
+Ltac isZcst t :=
+  let t := eval hnf in t in
+  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 Ring Zr : Zth
+  (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]).
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 7526cc8a6..77653c3ac 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -151,8 +151,8 @@ let contrib_name = "setoid_ring"
 
 let ring_dir = ["Coq";contrib_name]
 let ring_modules = 
-  [ring_dir@["BinList"];ring_dir@["Ring_th"];ring_dir@["Pol"];
-   ring_dir@["Ring_tac"];ring_dir@["Field_tac"];ring_dir@["ZRing_th"]]
+  [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"];
@@ -165,20 +165,20 @@ let coq_constant 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@["ZRing_th";m]] c)
+  lazy (Coqlib.gen_constant_in_modules "Ring" [ring_dir@["InitialRing";m]] c)
 
 let new_ring_path =
   make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"])
 let ltac s =
   lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
 let znew_ring_path =
-  make_dirpath (List.map id_of_string ["ZRing_th";contrib_name;"Coq"])
+  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;"Pol"] s ;;
+let pol_cst s = mk_cst [contrib_name;"Ring_polynom"] s ;;
 
 (* Ring theory *)
 
@@ -714,11 +714,11 @@ TACTIC EXTEND setoid_ring
 END
 
 (***********************************************************************)
-let fld_cst s = mk_cst [contrib_name;"NewField"] s ;;
+let fld_cst s = mk_cst [contrib_name;"Field"] s ;;
 
 let field_modules = List.map
   (fun f -> ["Coq";contrib_name;f])
-  ["NewField";"Field_tac"]
+  ["Field";"Field_tac"]
 
 let new_field_path =
   make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"])
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 47be9d236..a21bfec44 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Export ZArith.
-Require Export NewZArithRing.
+Require Export ZArithRing.
 Require Export Setoid.
 
 (** * Definition of [Q] and basic properties *)
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 40c310ff4..ade0cd5eb 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import NewField Field_tac.
+Require Import Field Field_tac.
 Require Import QArith.
 Require Import Znumtheory.
 Require Import Eqdep_dec.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index c05ea465d..a00d42879 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,7 +12,7 @@ Require Import Rbase.
 Require Import Rbasic_fun.
 Require Import Even.
 Require Import Div2.
-Require Import NewArithRing.
+Require Import ArithRing.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 3b5d241fa..c6feb4ac6 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,9 +13,9 @@
 (***************************************************************************)
 
 Require Export Raxioms.
-Require Export NewZArithRing.
+Require Export ZArithRing.
 Require Import Omega.
-Require Export Field_tac. Import NewField.
+Require Export Field_tac. Import Field.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
@@ -88,7 +88,7 @@ apply Rlt_trans with (0 + 1).
   apply Rplus_0_l.
 Qed.
 
-Lemma Rgen_phiPOS : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x > 0.
+Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
 unfold Rgt in |- *.
 induction x; simpl in |- *; intros.
  apply Rlt_trans with (1 + 0).
@@ -111,7 +111,8 @@ induction x; simpl in |- *; intros.
 Qed.
 
 
-Lemma Rgen_phiPOS_not_0 : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x <> 0.
+Lemma Rgen_phiPOS_not_0 :
+  forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.
 red in |- *; intros.
 specialize (Rgen_phiPOS x).
 rewrite H in |- *; intro.
@@ -119,8 +120,8 @@ apply (Rlt_asym 0 0); trivial.
 Qed.
 
 Lemma Zeq_bool_complete : forall x y, 
-  ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
-  ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
+  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
+  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
   Zeq_bool x y = true.
 Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0.
 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 878d5f73d..99c804272 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -15,8 +15,8 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
-Require Export ArithRing. (* for ring_nat... *)
-Require Export NewArithRing.
+Require Export LegacyArithRing. (* for ring_nat... *)
+Require Export ArithRing.
 
 Require Import Rbase.
 Require Export R_Ifp.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 718ac3b03..a3f17f4d8 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,8 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import NewZArithRing.
-
+Require Import ZArithRing.
 Require Import ZArith_base.
 Require Import Omega.
 Require Import Wf_nat.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 52f85eada..d08515e62 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -22,7 +22,7 @@ Then only after proves the main required property.
 Require Export ZArith_base.
 Require Import Zbool.
 Require Import Omega.
-Require Import NewZArithRing.
+Require Import ZArithRing.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 14bfa6357..9ae354eae 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Import ZArith_base.
-Require Import NewZArithRing.
+Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
 Require Import Ndigits.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 3d57561ea..804ab679d 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Import NewZArithRing.
+Require Import ZArithRing.
 Require Import Omega.
 Require Export ZArith_base.
 Open Local Scope Z_scope.