Ajout de Field

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

10 files changed, 1151 insertions, 53 deletions

diff --git a/.depend b/.depend
index 39166699b9..13b4364e1c 100644
--- a/.depend
+++ b/.depend
@@ -1622,6 +1622,18 @@ contrib/extraction/ocaml.cmx: kernel/environ.cmx library/global.cmx \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
     kernel/names.cmx lib/pp.cmx lib/pp_control.cmx kernel/term.cmx \
     lib/util.cmx contrib/extraction/ocaml.cmi 
+contrib/field/field.cmo: parsing/astterm.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
+    library/libobject.cmi kernel/names.cmi library/nametab.cmi \
+    proofs/proof_type.cmi contrib/ring/quote.cmo contrib/ring/ring.cmo \
+    library/summary.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi 
+contrib/field/field.cmx: parsing/astterm.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/evd.cmx library/global.cmx library/lib.cmx \
+    library/libobject.cmx kernel/names.cmx library/nametab.cmx \
+    proofs/proof_type.cmx contrib/ring/quote.cmx contrib/ring/ring.cmx \
+    library/summary.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx 
 contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     parsing/astterm.cmi pretyping/classops.cmi toplevel/command.cmi \
     parsing/coqast.cmi contrib/interface/dad.cmi \
@@ -1858,6 +1870,7 @@ contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/xml/xmlcommand.cmx 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
 contrib/correctness/psyntax.cmo: parsing/grammar.cma
+contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
 parsing/lexer.cmo: 
 parsing/q_coqast.cmo: 
 parsing/g_prim.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index 5fa3abb6a0..e30a54d290 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,5 +1,6 @@
 tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
 contrib/correctness/psyntax.ml: parsing/grammar.cma
+contrib/field/field.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
 parsing/lexer.ml: 
 parsing/q_coqast.ml: 
 parsing/g_prim.ml: 
diff --git a/.depend.coq b/.depend.coq
index bac71a85f5..6aa06d8fb3 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -51,7 +51,7 @@ theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo t
 theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
 theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo
 theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
-theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/Zarith/ZArith.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
 theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Num/SubProps.vo: theories/Num/SubProps.v
@@ -74,6 +74,7 @@ theories/Num/DiscrAxioms.vo: theories/Num/DiscrAxioms.v theories/Num/Params.vo t
 theories/Num/Definitions.vo: theories/Num/Definitions.v
 theories/Num/Axioms.vo: theories/Num/Axioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo
 theories/Num/AddProps.vo: theories/Num/AddProps.v theories/Num/Axioms.vo theories/Num/EqAxioms.vo
+theories/Logic/JMeq.vo: theories/Logic/JMeq.v
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
 theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
 theories/Logic/Decidable.vo: theories/Logic/Decidable.v
@@ -149,15 +150,18 @@ test-suite/success/evars.vo: test-suite/success/evars.v
 test-suite/success/eqdecide.vo: test-suite/success/eqdecide.v
 test-suite/success/eauto.vo: test-suite/success/eauto.v theories/Lists/PolyList.vo
 test-suite/success/Tauto.vo: test-suite/success/Tauto.v
+test-suite/success/Decompose.vo: test-suite/success/Decompose.v
 test-suite/success/Check.vo: test-suite/success/Check.v
 test-suite/success/Cases.vo: test-suite/success/Cases.v theories/Bool/Bool.vo theories/Arith/Peano_dec.vo theories/Init/Prelude.vo theories/Init/Logic_TypeSyntax.vo theories/Init/Logic_Type.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo
 test-suite/success/Apply.vo: test-suite/success/Apply.v
 test-suite/failure/search.vo: test-suite/failure/search.v
 test-suite/failure/redef.vo: test-suite/failure/redef.v
 test-suite/failure/positivity.vo: test-suite/failure/positivity.v
+test-suite/failure/params_ind.vo: test-suite/failure/params_ind.v
 test-suite/failure/illtype1.vo: test-suite/failure/illtype1.v
 test-suite/failure/fixpoint1.vo: test-suite/failure/fixpoint1.v
 test-suite/failure/clash_cons.vo: test-suite/failure/clash_cons.v
+test-suite/failure/check.vo: test-suite/failure/check.v
 test-suite/failure/Tauto.vo: test-suite/failure/Tauto.v
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
 test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
@@ -174,8 +178,12 @@ contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.v
 contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
 contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
-contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo contrib/interface/AddDad.vo
+contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v
+contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
+contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo
+contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
+contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/field/field.cmo
 contrib/extraction/test_extraction.vo: contrib/extraction/test_extraction.v
 contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v
 contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo
@@ -188,7 +196,7 @@ contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/Zarith/ZA
 contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Zarith/ZArith.vo theories/Bool/Sumbool.vo
 contrib/correctness/MakeProgramsState.vo: contrib/correctness/MakeProgramsState.v
 contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
-contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo contrib/correctness/pmisc.cmo contrib/correctness/peffect.cmo contrib/correctness/prename.cmo contrib/correctness/perror.cmo contrib/correctness/penv.cmo contrib/correctness/putil.cmo contrib/correctness/pdb.cmo contrib/correctness/pcic.cmo contrib/correctness/pmonad.cmo contrib/correctness/pcicenv.cmo contrib/correctness/pred.cmo contrib/correctness/ptyping.cmo contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo contrib/correctness/ptactic.cmo contrib/correctness/psyntax.cmo
+contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
 contrib/correctness/Arrays_stuff.vo: contrib/correctness/Arrays_stuff.v contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo contrib/correctness/Sorted.vo
 contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
 contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
@@ -204,59 +212,63 @@ syntax/PPConstr.vo: syntax/PPConstr.v
 syntax/PPCases.vo: syntax/PPCases.v
 syntax/MakeBare.vo: syntax/MakeBare.v
 states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo test-suite/success/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo tactics/EqDecide.vo contrib/extraction/Extraction.vo
-contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo contrib/interface/AddDad.vo
+contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo
+contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo
+contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/field/field.cmo
+contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
+contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v
-contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
-contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo contrib/correctness/pmisc.cmo contrib/correctness/peffect.cmo contrib/correctness/prename.cmo contrib/correctness/perror.cmo contrib/correctness/penv.cmo contrib/correctness/putil.cmo contrib/correctness/pdb.cmo contrib/correctness/pcic.cmo contrib/correctness/pmonad.cmo contrib/correctness/pcicenv.cmo contrib/correctness/pred.cmo contrib/correctness/ptyping.cmo contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo contrib/correctness/ptactic.cmo contrib/correctness/psyntax.cmo
-contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/Zarith/ZArith.vo theories/Arith/Wf_nat.vo
+contrib/correctness/examples/fact_int.vo: contrib/correctness/examples/fact_int.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo
+contrib/correctness/examples/fact.vo: contrib/correctness/examples/fact.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo theories/Arith/Arith.vo
+contrib/correctness/examples/extract.vo: contrib/correctness/examples/extract.v contrib/correctness/ProgramsExtraction.vo contrib/correctness/examples/exp.vo contrib/correctness/examples/exp_int.vo contrib/correctness/examples/fact.vo contrib/correctness/examples/fact_int.vo contrib/correctness/examples/Handbook.vo
+contrib/correctness/examples/exp_int.vo: contrib/correctness/examples/exp_int.v contrib/omega/Zpower.vo contrib/omega/Zcomplements.vo contrib/correctness/Correctness.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+contrib/correctness/examples/exp.vo: contrib/correctness/examples/exp.v theories/Arith/Even.vo theories/Arith/Div2.vo contrib/correctness/Correctness.vo contrib/ring/ArithRing.vo contrib/ring/ZArithRing.vo
+contrib/correctness/examples/Handbook.vo: contrib/correctness/examples/Handbook.v contrib/correctness/Correctness.vo theories/Bool/Sumbool.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
+contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo
+contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
+contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 contrib/correctness/Programs_stuff.vo: contrib/correctness/Programs_stuff.v contrib/correctness/Arrays_stuff.vo
 contrib/correctness/ProgramsExtraction.vo: contrib/correctness/ProgramsExtraction.v contrib/extraction/Extraction.vo contrib/correctness/Correctness.vo contrib/correctness/pextract.cmo
+contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/Zarith/ZArith.vo theories/Arith/Wf_nat.vo
 contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/Zarith/ZArith.vo theories/Zarith/ZArith_dec.vo
 contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Zarith/ZArith.vo theories/Bool/Sumbool.vo
-contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo
-contrib/correctness/examples/make_extr.vo: contrib/correctness/examples/make_extr.v contrib/correctness/ProgramsExtraction.vo contrib/correctness/examples/exp.vo contrib/correctness/examples/exp_int.vo contrib/correctness/examples/fact.vo contrib/correctness/examples/fact_int.vo contrib/correctness/examples/Handbook.vo
-contrib/correctness/examples/Handbook.vo: contrib/correctness/examples/Handbook.v theories/Bool/Sumbool.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
-contrib/correctness/examples/fact.vo: contrib/correctness/examples/fact.v contrib/omega/Omega.vo theories/Arith/Arith.vo
-contrib/correctness/examples/fact_int.vo: contrib/correctness/examples/fact_int.v contrib/omega/Omega.vo contrib/ring/ZArithRing.vo
-contrib/correctness/examples/exp.vo: contrib/correctness/examples/exp.v theories/Arith/Even.vo theories/Arith/Div2.vo contrib/correctness/Correctness.vo contrib/ring/ArithRing.vo contrib/ring/ZArithRing.vo
-contrib/correctness/examples/exp_int.vo: contrib/correctness/examples/exp_int.v contrib/omega/Zpower.vo contrib/omega/Zcomplements.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 contrib/correctness/MakeProgramsState.vo: contrib/correctness/MakeProgramsState.v
 contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo
-contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
+contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo
 contrib/correctness/Arrays_stuff.vo: contrib/correctness/Arrays_stuff.v contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo contrib/correctness/Sorted.vo
-contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
-contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
+contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo
+contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo
 contrib/extraction/test/bench.vo: contrib/extraction/test/bench.v theories/Lists/PolyList.vo theories/Zarith/ZArith.vo theories/Arith/Even.vo
 contrib/extraction/test_extraction.vo: contrib/extraction/test_extraction.v
 contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v
 contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
+contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
-contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
+contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.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/Ring.vo: contrib/ring/Ring.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/ring.cmo
 contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo
-contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
-contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
 contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
+contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
+contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
 contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
-contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
 theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo
 theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo
 theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo
 theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo
 theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo
-theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
 theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
+theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo
+theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
 theories/IntMap/Map.vo: theories/IntMap/Map.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo
 theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/PolyList.vo theories/IntMap/Mapiter.vo
 theories/IntMap/Fset.vo: theories/IntMap/Fset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo
-theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
+theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo
 theories/IntMap/Adist.vo: theories/IntMap/Adist.v theories/Bool/Bool.vo theories/Zarith/ZArith.vo theories/Arith/Arith.vo theories/Arith/Min.vo theories/IntMap/Addr.vo
 theories/IntMap/Addr.vo: theories/IntMap/Addr.v theories/Bool/Bool.vo theories/Zarith/ZArith.vo
 theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo
-theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo
 theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
 theories/Num/Nat/NeqDef.vo: theories/Num/Nat/NeqDef.v theories/Num/Params.vo
 theories/Num/Nat/NSyntax.vo: theories/Num/Nat/NSyntax.v
@@ -265,54 +277,54 @@ theories/Num/Params.vo: theories/Num/Params.v
 theories/Num/NeqDef.vo: theories/Num/NeqDef.v theories/Num/Params.vo theories/Num/EqParams.vo
 theories/Num/EqParams.vo: theories/Num/EqParams.v theories/Num/Params.vo
 theories/Num/EqAxioms.vo: theories/Num/EqAxioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo
+theories/Num/Axioms.vo: theories/Num/Axioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo
 theories/Num/SubProps.vo: theories/Num/SubProps.v
 theories/Num/OppProps.vo: theories/Num/OppProps.v
+theories/Num/Leibniz/Params.vo: theories/Num/Leibniz/Params.v
+theories/Num/Leibniz/NSyntax.vo: theories/Num/Leibniz/NSyntax.v theories/Num/Params.vo
+theories/Num/Leibniz/EqAxioms.vo: theories/Num/Leibniz/EqAxioms.v theories/Num/NSyntax.vo
 theories/Num/OppAxioms.vo: theories/Num/OppAxioms.v
 theories/Num/NSyntax.vo: theories/Num/NSyntax.v theories/Num/Params.vo
-theories/Num/LtProps.vo: theories/Num/LtProps.v theories/Num/Axioms.vo theories/Num/AddProps.vo
-theories/Num/LeProps.vo: theories/Num/LeProps.v theories/Num/LtProps.vo theories/Num/LeAxioms.vo
 theories/Num/LeAxioms.vo: theories/Num/LeAxioms.v theories/Num/Axioms.vo theories/Num/LtProps.vo
-theories/Num/GtProps.vo: theories/Num/GtProps.v
+theories/Num/LtProps.vo: theories/Num/LtProps.v theories/Num/Axioms.vo theories/Num/AddProps.vo
 theories/Num/GtAxioms.vo: theories/Num/GtAxioms.v theories/Num/Axioms.vo theories/Num/LeProps.vo
-theories/Num/GeProps.vo: theories/Num/GeProps.v
+theories/Num/GtProps.vo: theories/Num/GtProps.v
 theories/Num/GeAxioms.vo: theories/Num/GeAxioms.v theories/Num/Axioms.vo theories/Num/LtProps.vo
 theories/Num/DiscrProps.vo: theories/Num/DiscrProps.v theories/Num/DiscrAxioms.vo theories/Num/LtProps.vo
-theories/Num/Leibniz/Params.vo: theories/Num/Leibniz/Params.v
-theories/Num/Leibniz/NSyntax.vo: theories/Num/Leibniz/NSyntax.v theories/Num/Params.vo
-theories/Num/Leibniz/EqAxioms.vo: theories/Num/Leibniz/EqAxioms.v theories/Num/NSyntax.vo
 theories/Num/DiscrAxioms.vo: theories/Num/DiscrAxioms.v theories/Num/Params.vo theories/Num/NSyntax.vo
-theories/Num/Axioms.vo: theories/Num/Axioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo
-theories/Num/AddProps.vo: theories/Num/AddProps.v theories/Num/Axioms.vo theories/Num/EqAxioms.vo
 theories/Num/Definitions.vo: theories/Num/Definitions.v
-theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
+theories/Num/LeProps.vo: theories/Num/LeProps.v theories/Num/LtProps.vo theories/Num/LeAxioms.vo
+theories/Num/GeProps.vo: theories/Num/GeProps.v
+theories/Num/AddProps.vo: theories/Num/AddProps.v theories/Num/Axioms.vo theories/Num/EqAxioms.vo
 theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
+theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
 theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
+theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
 theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo
 theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo
 theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
 theories/Zarith/Wf_Z.vo: theories/Zarith/Wf_Z.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
-theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
+theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo
 theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theories/Logic/Eqdep.vo
 theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/Relation_Operators.vo theories/Relations/Relation_Definitions.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Transitive_Closure.vo: theories/Wellfounded/Transitive_Closure.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 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/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexicographic_Exponentiation.v theories/Logic/Eqdep.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo
 theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v
 theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo
 theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo
+theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
 theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
 theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
 theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
 theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
 theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
 theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
-theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
-theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
+theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
 theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
+theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
 theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
 theories/Sets/Permut.vo: theories/Sets/Permut.v
-theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
 theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
 theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
 theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
@@ -329,17 +341,18 @@ theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.
 theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
 theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
-theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
 theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
+theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo
+theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
 theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo
 theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo
 theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo
-theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/Zarith/ZArith.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
+theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
+theories/Logic/JMeq.vo: theories/Logic/JMeq.v
 theories/Logic/Decidable.vo: theories/Logic/Decidable.v
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
 theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
@@ -348,12 +361,13 @@ theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
 theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
 theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
 theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
+theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
 theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
 theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
-theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
-theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
+theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
 theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
 theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
@@ -363,13 +377,12 @@ theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Ini
 theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
 theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
-theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
 theories/Init/Datatypes.vo: theories/Init/Datatypes.v
 theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
 theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
-theories/Bool/Bool.vo: theories/Bool/Bool.v
 theories/Bool/DecBool.vo: theories/Bool/DecBool.v
+theories/Bool/Bool.vo: theories/Bool/Bool.v
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable.vo
@@ -387,5 +400,5 @@ theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arit
 theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Logic/Decidable.vo
 theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
-theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo
diff --git a/Makefile b/Makefile
index 7e7d0b1b2c..c0b42ced10 100644
--- a/Makefile
+++ b/Makefile
@@ -196,10 +196,10 @@ PARSERREQUIRES=lib/pp_control.cmo lib/pp.cmo \
 	parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
 	toplevel/errors.cmo
 
-ML4FILES += contrib/correctness/psyntax.ml4
+ML4FILES += contrib/correctness/psyntax.ml4 contrib/field/field.ml4
 
 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
-        contrib/ring/quote.cmo contrib/ring/ring.cmo \
+        contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/field/field.cmo \
 	contrib/xml/xml.cmo \
 	contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo \
 	$(EXTRACTIONCMO) $(CORRECTNESSCMO)
@@ -459,6 +459,9 @@ RINGVO = contrib/ring/ArithRing.vo      contrib/ring/Ring_normalize.vo \
          contrib/ring/ZArithRing.vo     contrib/ring/Ring_abstract.vo \
          contrib/ring/Quote.vo
 
+FIELDVO = contrib/field/Field_Compl.vo     contrib/field/Field_Theory.vo \
+          contrib/field/Field_Tactic.vo    contrib/field/Field.vo
+
 XMLVO = contrib/xml/Xml.vo
 
 INTERFACEV0 = contrib/interface/Centaur.vo
@@ -469,7 +472,8 @@ contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
 contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE)
 	$(COQC) -q -byte -bindir bin $(COQINCLUDES) $<
 
-CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO) $(CORRECTNESSVO) $(INTERFACEV0)
+CONTRIBVO = $(OMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\
+            $(INTERFACEV0)
 
 $(CONTRIBVO): states/initial.coq
 
diff --git a/contrib/field/Field.v b/contrib/field/Field.v
new file mode 100644
index 0000000000..1e5baf0167
--- /dev/null
+++ b/contrib/field/Field.v
@@ -0,0 +1,33 @@
+(* Field.v *)
+
+Require Export Field_Compl.
+Require Export Field_Theory.
+Require Export Field_Tactic.
+
+Declare ML Module "field".
+
+Grammar vernac opt_arg_list : List :=
+| noal [] -> []
+| minus [ "minus" ":=" constrarg($aminus) opt_arg_list($l) ] ->
+  [ "minus" $aminus ($LIST $l) ]
+| div [ "div" ":=" constrarg($adiv) opt_arg_list($l) ] ->
+  [ "div" $adiv ($LIST $l) ]
+
+with extra_args : List :=
+| nea [] -> []
+| with_a [ "with" opt_arg_list($l)] -> [ ($LIST $l) ]
+
+with vernac : ast := 
+  addfield [ "Add" "Field" 
+      	     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
+      	     constrarg($azero) constrarg($aopp) constrarg($aeq)
+             constrarg($ainv) constrarg($rth) constrarg($ainv_l) extra_args($l)
+             "." ]
+    -> [(AddField $a $aplus $amult $aone $azero $aopp $aeq $ainv $rth
+                  $ainv_l ($LIST $l))].
+
+Grammar tactic simple_tactic: ast :=
+  | field [ "Field" ] -> [(Field)].
+
+Syntax tactic level 0:
+  | field [(Field)] -> ["Field"].
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
new file mode 100644
index 0000000000..d18d19f764
--- /dev/null
+++ b/contrib/field/Field_Compl.v
@@ -0,0 +1,57 @@
+(* Field_Compl.v *)
+
+Inductive list [A:Type] : Type :=
+  nil : (list A) | cons : A->(list A)->(list A).
+
+Fixpoint app [A:Type][l:(list A)] : (list A) -> (list A) :=
+  [m:(list A)]
+  Cases l of
+  | nil => m 
+  | (cons a l1) => (cons A a (app A l1 m))
+  end.
+
+Inductive Sprod [A:Type;B:Set] : Type :=
+  Spair : A -> B -> (Sprod A B).
+
+Definition assoc_2nd :=
+Fix assoc_2nd_rec {assoc_2nd_rec/4:
+  (A:Type)(B:Set)((e1,e2:B){e1=e2}+{~e1=e2})->(list (Sprod A B))->B->A->A:=
+    [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(list (Sprod A B));
+      key:B;default:A]
+  Cases lst of
+  | nil => default
+  | (cons (Spair v e) l) =>
+    (Cases (eq_dec e key) of
+    | (left _) => v
+    | (right _) => (assoc_2nd_rec A B eq_dec l key default)
+    end)
+  end}.
+
+Inductive prodT [A,B:Type] : Type :=
+  pairT: A->B->(prodT A B).
+
+Definition fstT [A,B:Type;c:(prodT A B)] :=
+  Cases c of
+  | (pairT a _) => a
+  end.
+
+Definition sndT [A,B:Type;c:(prodT A B)] :=
+  Cases c of
+  | (pairT _ a) => a
+  end.
+
+Definition mem :=
+Fix mem {mem/4:(A:Set)((e1,e2:A){e1=e2}+{~e1=e2})->(a:A)(list A)->bool :=
+  [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(list A)]
+  Cases l of
+  | nil => false
+  | (cons a1 l1) =>
+    Cases (eq_dec a a1) of
+    | (left _) => true
+    | (right _) => (mem A eq_dec a l1)
+    end
+  end}.
+
+Inductive option [A:Type] : Type :=
+  | None : (option A)
+  | Some : (A -> A -> A) -> (option A).
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
new file mode 100644
index 0000000000..d0644e8d60
--- /dev/null
+++ b/contrib/field/Field_Tactic.v
@@ -0,0 +1,251 @@
+(* Field_Tactic.v *)
+
+Require Ring.
+(*Require Export Field_Compl.
+Require Export Field_Theory.*)
+
+(**** Interpretation A --> ExprA ****)
+
+Recursive Tactic Definition MemAssoc var lvar :=
+  Match lvar With
+  | [(nil ?)] -> false
+  | [(cons ? ?1 ?2)] ->
+    (Match ?1==var With
+     | [?1== ?1] -> true
+     | _ -> (MemAssoc var ?2)).
+
+Recursive Tactic Definition SeekVarAux FT lvar trm :=
+  Let AT     = Eval Compute in (A FT)
+  And AzeroT = Eval Compute in (Azero FT)
+  And AoneT  = Eval Compute in (Aone FT)
+  And AplusT = Eval Compute in (Aplus FT)
+  And AmultT = Eval Compute in (Amult FT)
+  And AoppT  = Eval Compute in (Aopp FT)
+  And AinvT  = Eval Compute in (Ainv FT) In
+  Match trm With
+  | [(AzeroT)] -> lvar
+  | [(AoneT)] -> lvar
+  | [(AplusT ?1 ?2)] ->
+    Let l1 = (SeekVarAux FT lvar ?1) In
+    (SeekVarAux FT l1 ?2)
+  | [(AmultT ?1 ?2)] ->
+    Let l1 = (SeekVarAux FT lvar ?1) In
+    (SeekVarAux FT l1 ?2)
+  | [(AoppT ?1)] -> (SeekVarAux FT lvar ?1)
+  | [(AinvT ?1)] -> (SeekVarAux FT lvar ?1)
+  | [?1] ->
+    Let res = (MemAssoc ?1 lvar) In
+    Match res With
+    | [(true)] -> lvar
+    | [(false)] -> '(cons AT ?1 lvar).
+
+Tactic Definition SeekVar FT trm :=
+  Let AT = Eval Compute in (A FT) In
+  (SeekVarAux FT '(nil AT) trm).
+
+Recursive Tactic Definition NumberAux lvar cpt :=
+  Match lvar With
+  | [(nil ?1)] -> '(nil (Sprod ?1 nat))
+  | [(cons ?1 ?2 ?3)] ->
+    Let l2 = (NumberAux ?3 '(S cpt)) In
+    '(cons (Sprod ?1 nat) (Spair ?1 nat ?2 cpt) l2).
+
+Tactic Definition Number lvar := (NumberAux lvar O).
+
+Tactic Definition BuildVarList FT trm :=
+  Let lvar = (SeekVar FT trm) In
+  (Number lvar).
+
+Recursive Tactic Definition Assoc elt lst :=
+  Match lst With
+  | [(nil ?)] -> Fail
+  | [(cons (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
+    Match elt== ?1 With
+    | [?1== ?1] -> ?2
+    | _ -> (Assoc elt ?3).
+
+Recursive Tactic Definition interp_A FT lvar trm :=
+  Let AT     = Eval Compute in (A FT)
+  And AzeroT = Eval Compute in (Azero FT)
+  And AoneT  = Eval Compute in (Aone FT)
+  And AplusT = Eval Compute in (Aplus FT)
+  And AmultT = Eval Compute in (Amult FT)
+  And AoppT  = Eval Compute in (Aopp FT)
+  And AinvT  = Eval Compute in (Ainv FT) In
+  Match trm With
+  | [(AzeroT)] -> EAzero
+  | [(AoneT)] -> EAone
+  | [(AplusT ?1 ?2)] ->
+    Let e1 = (interp_A FT lvar ?1)
+    And e2 = (interp_A FT lvar ?2) In
+    '(EAplus e1 e2)
+  | [(AmultT ?1 ?2)] ->
+    Let e1 = (interp_A FT lvar ?1)
+    And e2 = (interp_A FT lvar ?2) In
+    '(EAmult e1 e2)
+  | [(AoppT ?1)] ->
+    Let e = (interp_A FT lvar ?1) In
+    '(EAopp e)
+  | [(AinvT ?1)] ->
+    Let e = (interp_A FT lvar ?1) In
+    '(EAinv e)
+  | [?1] ->
+    Let idx = (Assoc ?1 lvar) In
+    '(EAvar idx).
+
+(************************)
+(*    Simplification    *)
+(************************)
+
+(**** Generation of the multiplier ****)
+
+Recursive Tactic Definition Remove e l :=
+  Match l With
+  | [(nil ?)] -> l
+  | [(cons ?1 e ?2)] -> ?2
+  | [(cons ?1 ?2 ?3)] ->
+    Let nl = (Remove e ?3) In
+    '(cons ?1 ?2 nl).
+
+Recursive Tactic Definition Union l1 l2 :=
+  Match l1 With
+  | [(nil ?)] -> l2
+  | [(cons ?1 ?2 ?3)] ->
+    Let nl2 = (Remove ?2 l2) In
+    Let nl = (Union ?3 nl2) In
+    '(cons ?1 ?2 nl).
+
+Recursive Tactic Definition RawGiveMult trm :=
+  Match trm With
+  | [(EAinv ?1)] -> '(cons ExprA ?1 (nil ExprA))
+  | [(EAopp ?1)] -> (RawGiveMult ?1)
+  | [(EAplus ?1 ?2)] ->
+    Let l1 = (RawGiveMult ?1)
+    And l2 = (RawGiveMult ?2) In
+    (Union l1 l2)
+  | [(EAmult ?1 ?2)] ->
+    Let l1 = (RawGiveMult ?1)
+    And l2 = (RawGiveMult ?2) In
+    Eval Compute in (app ExprA l1 l2)
+  | _ -> '(nil ExprA).
+
+Tactic Definition GiveMult trm :=
+  Let ltrm = (RawGiveMult trm) In
+  '(mult_of_list ltrm).
+
+(**** Associativity ****)
+
+Tactic Definition ApplyAssoc FT lvar trm :=
+  Cut (interp_ExprA FT lvar (assoc trm))==(interp_ExprA FT lvar trm);
+  [Intro;
+   (Match Context With
+    | [id:(interp_ExprA ? ? (assoc ?))== ? |- ?] ->
+      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |Apply assoc_correct].
+
+(**** Distribution *****)
+
+Tactic Definition ApplyDistrib FT lvar trm :=
+  Cut (interp_ExprA FT lvar (distrib trm))==(interp_ExprA FT lvar trm);
+  [Intro;
+   (Match Context With
+    | [id:(interp_ExprA ? ? (distrib ?))== ? |- ?] ->
+      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |Apply distrib_correct].
+
+(**** Multiplication by the inverse product ****)
+
+Tactic Definition GrepMult :=
+  Match Context With
+    | [ id: ~(interp_ExprA ? ? ?)== ? |- ?] -> id.
+
+Tactic Definition Multiply mul :=
+  Match Context With
+  | [|-(interp_ExprA ?1 ?2 ?3)==(interp_ExprA ?1 ?2 ?4)] ->
+    Let AzeroT = Eval Compute in (Azero ?1) In
+    Cut ~(interp_ExprA ?1 ?2 mul)==AzeroT;
+    [Intro;
+     Let id = GrepMult In
+     Apply (mult_eq ?1 ?3 ?4 mul ?2 id);
+     Cbv Beta Delta -[interp_ExprA] Iota
+    |Cbv Beta Delta -[not] Iota;
+     Let AmultT = Eval Compute in (Amult ?1)
+     And AoneT = Eval Compute in (Aone ?1) In
+     (Match Context With
+      | [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1))].
+
+Tactic Definition ApplyMultiply FT lvar trm :=
+  Cut (interp_ExprA FT lvar (multiply trm))==(interp_ExprA FT lvar trm);
+  [Intro;
+   (Match Context With
+    | [id:(interp_ExprA ? ? (multiply ?))== ? |- ?] ->
+      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |Apply multiply_correct].
+
+(**** Permutations and simplification ****)
+
+Tactic Definition ApplyInverse mul FT lvar trm :=
+  Cut (interp_ExprA FT lvar (inverse_simplif mul trm))==
+      (interp_ExprA FT lvar trm);
+  [Intro;
+   (Match Context With
+   | [id:(interp_ExprA ? ? (inverse_simplif ? ?))== ? |- ?] ->
+     Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |Apply inverse_correct;Assumption].
+
+(**** Inverse test ****)
+
+Tactic Definition InverseTestAux FT trm :=
+  Let AplusT = Eval Compute in (Aplus FT)
+  And AmultT = Eval Compute in (Amult FT)
+  And AoppT  = Eval Compute in (Aopp FT)
+  And AinvT  = Eval Compute in (Ainv FT) In
+  Match trm With
+  | [(AinvT ?)] -> Fail
+  | [(AoppT ?1)] -> (InverseTestAux FT ?1)
+  | [(AplusT ?1 ?2)] -> (InverseTestAux FT ?1);(InverseTestAux FT ?2)
+  | [(AmultT ?1 ?2)] -> (InverseTestAux FT ?1);(InverseTestAux FT ?2)
+  | _ -> Idtac.
+
+Tactic Definition InverseTest FT :=
+  Let AplusT = Eval Compute in (Aplus FT) In
+  Match Context With
+  | [|-?1== ?2] -> (InverseTestAux FT '(AplusT ?1 ?2)).
+
+(**** Field itself ****)
+
+Tactic Definition ApplySimplif sfun :=
+(*  Match Context With
+  | [ |- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ?4 ?5) ] ->
+    (sfun ?1 ?2 ?3);(sfun ?1 ?4 ?5).*)
+  (Match Context With
+   | [ |- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ? ?) ] ->
+     (sfun ?1 ?2 ?3));
+  (Match Context With
+   | [ |- (interp_ExprA ? ? ?)==(interp_ExprA ?1 ?2 ?3) ] ->
+     (sfun ?1 ?2 ?3)).
+
+Tactic Definition Unfolds FT :=
+  (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With
+   | [(Some ? ?1)] -> Unfold ?1
+   | _ -> Idtac);
+  (Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With
+   | [(Some ? ?1)] -> Unfold ?1
+   | _ -> Idtac).
+
+Tactic Definition Field_Gen FT :=
+  Let AplusT = Eval Compute in (Aplus FT) In
+  Unfolds FT;
+  Match Context With
+  | [|-?1== ?2] ->
+    Let lvar = (BuildVarList FT '(AplusT ?1 ?2)) In
+    Let trm1 = (interp_A FT lvar ?1)
+    And trm2 = (interp_A FT lvar ?2) In
+    Let mul = (GiveMult '(EAplus trm1 trm2)) In
+    Cut (interp_ExprA FT lvar trm1)==(interp_ExprA FT lvar trm2);
+    [Compute;Auto
+    |(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
+     (Multiply mul);[(ApplySimplif ApplyMultiply);
+       (ApplySimplif (ApplyInverse mul));
+       (Let id = GrepMult In Clear id);Compute;
+       First [(InverseTest FT);Ring|(Field_Gen FT)]|Idtac]].
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
new file mode 100644
index 0000000000..4baa98f6bc
--- /dev/null
+++ b/contrib/field/Field_Theory.v
@@ -0,0 +1,611 @@
+(* Field_Theory.v *)
+
+Require Peano_dec.
+Require Ring.
+Require Field_Compl.
+
+Record Field_Theory : Type :=
+{ A : Type;
+  Aplus : A -> A -> A;
+  Amult : A -> A -> A;
+  Aone : A;
+  Azero : A;
+  Aopp : A -> A;
+  Aeq : A -> A -> bool;
+  Ainv : A -> A;
+  Aminus : (option A);
+  Adiv : (option A);
+  RT : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq);
+  Th_inv_def : (n:A)~(n==Azero)->(Amult (Ainv n) n)==Aone
+}.
+
+(* The reflexion structure *)
+Inductive ExprA : Set :=
+| EAzero    : ExprA
+| EAone    : ExprA
+| EAplus : ExprA -> ExprA -> ExprA
+| EAmult : ExprA -> ExprA -> ExprA
+| EAopp  : ExprA -> ExprA
+| EAinv  : ExprA -> ExprA
+| EAvar  : nat -> ExprA.
+
+(**** Decidability of equality ****)
+
+Lemma eqExprA_O:(e1,e2:ExprA){e1=e2}+{~e1=e2}.
+Proof.
+  Double Induction 1 2;Try Intros;
+   Try (Left;Reflexivity) Orelse Try (Right;Discriminate).
+  Elim (H1 e0);Intro y;Elim (H2 e);Intro y0;
+    Try (Left; Rewrite y; Rewrite y0;Auto)
+    Orelse (Right;Red;Intro;Inversion H3;Auto).
+  Elim (H1 e0);Intro y;Elim (H2 e);Intro y0;
+    Try (Left; Rewrite y; Rewrite y0;Auto)
+    Orelse (Right;Red;Intro;Inversion H3;Auto).
+  Elim (H0 e);Intro y.
+  Left; Rewrite y; Auto.
+  Right;Red; Intro;Inversion H1;Auto.
+  Elim (H0 e);Intro y.
+  Left; Rewrite y; Auto.
+  Right;Red; Intro;Inversion H1;Auto.
+  Elim (eq_nat_dec n n0);Intro y.
+  Left; Rewrite y; Auto.
+  Right;Red;Intro;Inversion H;Auto. 
+Save.
+
+Transparent Peano_dec.eq_nat_dec.
+Transparent eqExprA_O.
+
+Definition eq_nat_dec := Eval Compute in Peano_dec.eq_nat_dec.
+Definition eqExprA := Eval Compute in eqExprA_O.
+
+(**** Generation of the multiplier ****)
+
+Fixpoint mult_of_list [e:(list ExprA)]: ExprA :=
+  Cases e of
+  | nil => EAone
+  | (cons e1 l1) => (EAmult e1 (mult_of_list l1))
+  end.
+
+Section Theory_of_fields.
+
+Variable T : Field_Theory.
+
+Local AT := (A T).
+Local AplusT := (Aplus T).
+Local AmultT := (Amult T).
+Local AoneT := (Aone T).
+Local AzeroT := (Azero T).
+Local AoppT := (Aopp T).
+Local AeqT := (Aeq T).
+Local AinvT := (Ainv T).
+Local RTT := (RT T).
+Local Th_inv_defT := (Th_inv_def T).
+
+Add Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (Azero T) (Aopp T) 
+  (Aeq T) (RT T).
+
+Add Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
+
+(***************************)
+(*    Lemmas to be used    *)
+(***************************)
+
+Lemma AplusT_sym:(r1,r2:AT)(AplusT r1 r2)==(AplusT r2 r1).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AplusT_assoc:(r1,r2,r3:AT)(AplusT (AplusT r1 r2) r3)==
+                                (AplusT r1 (AplusT r2 r3)).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_sym:(r1,r2:AT)(AmultT r1 r2)==(AmultT r2 r1).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_assoc:(r1,r2,r3:AT)(AmultT (AmultT r1 r2) r3)==
+                                (AmultT r1 (AmultT r2 r3)).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AplusT_Ol:(r:AT)(AplusT AzeroT r)==r.
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_1l:(r:AT)(AmultT AoneT r)==r.
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AplusT_AoppT_r:(r:AT)(AplusT r (AoppT r))==AzeroT.
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_AplusT_distr:(r1,r2,r3:AT)(AmultT r1 (AplusT r2 r3))==
+                        (AplusT (AmultT r1 r2) (AmultT r1 r3)).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma r_AplusT_plus:(r,r1,r2:AT)(AplusT r r1)==(AplusT r r2)->r1==r2.
+Proof.
+  Intros; Transitivity (AplusT (AplusT (AoppT r) r) r1).
+  Ring.
+  Transitivity (AplusT (AplusT (AoppT r) r) r2).
+  Repeat Rewrite -> AplusT_assoc; Rewrite <- H; Reflexivity.
+  Ring.
+Save.
+ 
+Lemma r_AmultT_mult:
+  (r,r1,r2:AT)(AmultT r r1)==(AmultT r r2)->~r==AzeroT->r1==r2.
+Proof.
+  Intros; Transitivity (AmultT (AmultT (AinvT r) r) r1).
+  Rewrite Th_inv_defT;[Symmetry; Apply AmultT_1l;Auto|Auto].
+  Transitivity (AmultT (AmultT (AinvT r) r) r2).
+  Repeat Rewrite AmultT_assoc; Rewrite H; Trivial.
+  Rewrite Th_inv_defT;[Apply AmultT_1l;Auto|Auto].
+Save.
+
+Lemma AmultT_Or:(r:AT) (AmultT r AzeroT)==AzeroT.
+Proof.
+  Intro; Ring.
+Save.
+ 
+Lemma AmultT_Ol:(r:AT)(AmultT AzeroT r)==AzeroT.
+Proof.
+  Intro; Ring.
+Save.
+ 
+Lemma AmultT_1r:(r:AT)(AmultT r AoneT)==r.
+Proof.
+  Intro; Ring.
+Save.
+ 
+Lemma AinvT_r:(r:AT)~r==AzeroT->(AmultT r (AinvT r))==AoneT.
+Proof.
+  Intros; Rewrite -> AmultT_sym; Apply Th_inv_defT; Auto.
+Save.
+ 
+Lemma without_div_O_contr:
+  (r1,r2:AT)~(AmultT r1 r2)==AzeroT ->~r1==AzeroT/\~r2==AzeroT.
+Proof.
+  Intros r1 r2 H; Split; Red; Intro; Apply H; Rewrite H0; Ring.
+Save.
+
+(************************)
+(*    Interpretation    *)
+(************************)
+
+(**** ExprA --> A ****)
+
+Fixpoint interp_ExprA [lvar:(list (Sprod AT nat));e:ExprA] : AT :=
+  Cases e of
+  | EAzero            => AzeroT
+  | EAone            => AoneT
+  | (EAplus e1 e2) => (AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2))
+  | (EAmult e1 e2) => (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2))
+  | (EAopp e)      => ((Aopp T) (interp_ExprA lvar e))
+  | (EAinv e)      => ((Ainv T) (interp_ExprA lvar e))
+  | (EAvar n)      => (assoc_2nd AT nat eq_nat_dec lvar n AzeroT)
+  end.
+
+(************************)
+(*    Simplification    *)
+(************************)
+
+(**** Associativity ****)
+
+Definition merge_mult :=
+  Fix merge_mult {merge_mult/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAmult t1 t2) =>
+    Cases t2 of
+    | (EAmult t2 t3) => (EAmult t1 (EAmult t2 (merge_mult t3 e2)))
+    | _ => (EAmult t1 (EAmult t2 e2))
+    end
+  | _ => (EAmult e1 e2)
+  end}.
+
+Fixpoint assoc_mult [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAmult e1 e3) =>
+    Cases e1 of
+    | (EAmult e1 e2) =>
+      (merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2))
+        (assoc_mult e3))
+    | _ => (EAmult e1 (assoc_mult e3))
+    end
+  | _ => e
+  end.
+
+Definition merge_plus :=
+  Fix merge_plus {merge_plus/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAplus t1 t2) =>
+    Cases t2 of
+    | (EAplus t2 t3) => (EAplus t1 (EAplus t2 (merge_plus t3 e2)))
+    | _ => (EAplus t1 (EAplus t2 e2))
+    end
+  | _ => (EAplus e1 e2)
+  end}.
+
+Fixpoint assoc [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e3) =>
+    Cases e1 of
+    | (EAplus e1 e2) =>
+      (merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3))
+    | _ => (EAplus (assoc_mult e1) (assoc e3))
+    end
+  | _ => (assoc_mult e)
+  end.
+
+Lemma merge_mult_correct1:
+  (e1,e2,e3:ExprA)(lvar:(list (Sprod AT nat)))
+  (interp_ExprA lvar (merge_mult (EAmult e1 e2) e3))==
+  (interp_ExprA lvar (EAmult e1 (merge_mult e2 e3))).
+Proof.
+Intros e1 e2;Generalize e1;Generalize e2;Clear e1 e2.
+Induction e2;Auto;Intros.
+Unfold 1 merge_mult;Fold merge_mult;
+ Unfold 2 interp_ExprA;Fold interp_ExprA;
+ Rewrite (H0 e e3 lvar);
+ Unfold 1 interp_ExprA;Fold interp_ExprA;
+ Unfold 5 interp_ExprA;Fold interp_ExprA;Auto.
+Save.
+
+Lemma merge_mult_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (merge_mult e1 e2))==
+    (interp_ExprA lvar (EAmult e1 e2)).
+Proof.
+Induction e1;Auto;Intros.
+Elim e0;Try (Intros;Simpl;Ring).
+Unfold interp_ExprA in H2;Fold interp_ExprA in H2;
+ Cut (AmultT (interp_ExprA lvar e2) (AmultT (interp_ExprA lvar e4) 
+       (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))))==
+       (AmultT (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) 
+       (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
+Intro H3;Rewrite H3;Rewrite <-H2;
+ Rewrite merge_mult_correct1;Simpl;Ring.
+Ring.
+Save.
+
+Lemma assoc_mult_correct1:(e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (AmultT (interp_ExprA lvar (assoc_mult e1)) 
+         (interp_ExprA lvar (assoc_mult e2)))==
+  (interp_ExprA lvar (assoc_mult (EAmult e1 e2))).
+Proof.
+Induction e1;Auto;Intros.
+Rewrite <-(H e0 lvar);Simpl;Rewrite merge_mult_correct;Simpl;
+ Rewrite merge_mult_correct;Simpl;Auto.
+Save.
+
+Lemma assoc_mult_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (assoc_mult e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Auto;Intros.
+Elim e0;Intros.
+Intros;Simpl;Ring.
+Simpl;Rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
+ Rewrite (AmultT_1l (interp_ExprA lvar e1)); Apply H0.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite merge_mult_correct;Simpl;Rewrite merge_mult_correct;Simpl;
+ Rewrite AmultT_assoc;Rewrite assoc_mult_correct1;Rewrite H2;Simpl;
+ Rewrite <-assoc_mult_correct1 in H1;
+ Unfold 3 interp_ExprA in H1;Fold interp_ExprA in H1;
+ Rewrite (H0 lvar) in H1;
+ Rewrite (AmultT_sym (interp_ExprA lvar e3) (interp_ExprA lvar e1));
+ Rewrite <-AmultT_assoc;Rewrite H1;Rewrite AmultT_assoc;Ring.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Save.
+
+Lemma merge_plus_correct1:
+  (e1,e2,e3:ExprA)(lvar:(list (Sprod AT nat)))
+  (interp_ExprA lvar (merge_plus (EAplus e1 e2) e3))==
+  (interp_ExprA lvar (EAplus e1 (merge_plus e2 e3))).
+Proof.
+Intros e1 e2;Generalize e1;Generalize e2;Clear e1 e2.
+Induction e2;Auto;Intros.
+Unfold 1 merge_plus;Fold merge_plus;
+ Unfold 2 interp_ExprA;Fold interp_ExprA;
+ Rewrite (H0 e e3 lvar);
+ Unfold 1 interp_ExprA;Fold interp_ExprA;
+ Unfold 5 interp_ExprA;Fold interp_ExprA;Auto.
+Save.
+
+Lemma merge_plus_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (merge_plus e1 e2))==
+    (interp_ExprA lvar (EAplus e1 e2)).
+Proof.
+Induction e1;Auto;Intros.
+Elim e0;Try Intros;Try (Simpl;Ring).
+Unfold interp_ExprA in H2;Fold interp_ExprA in H2;
+  Cut (AplusT (interp_ExprA lvar e2) (AplusT (interp_ExprA lvar e4) 
+        (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))))==
+        (AplusT (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) 
+       (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
+Intro H3;Rewrite H3;Rewrite <-H2;Rewrite merge_plus_correct1;Simpl;Ring.
+Ring.
+Save.
+
+Lemma assoc_plus_correct:(e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))==
+  (interp_ExprA lvar (assoc (EAplus e1 e2))).
+Proof.
+Induction e1;Auto;Intros.
+Rewrite <-(H e0 lvar);Simpl;Rewrite merge_plus_correct;Simpl;
+ Rewrite merge_plus_correct;Simpl;Auto.
+Save.
+
+Lemma assoc_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (assoc e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Auto;Intros.
+Elim e0;Intros.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite merge_plus_correct;Simpl;Rewrite merge_plus_correct;
+ Simpl;Rewrite AplusT_assoc;Rewrite assoc_plus_correct;Rewrite H2;
+ Simpl;Apply (r_AplusT_plus (interp_ExprA lvar (assoc e1))
+   (AplusT (interp_ExprA lvar (assoc e2))
+     (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1)))
+   (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3))
+        (interp_ExprA lvar e1)));Rewrite <-AplusT_assoc; 
+ Rewrite (AplusT_sym (interp_ExprA lvar (assoc e1)) 
+                    (interp_ExprA lvar (assoc e2)));
+ Rewrite assoc_plus_correct;Rewrite H1;Simpl;Rewrite (H0 lvar);
+ Rewrite <-(AplusT_assoc (AplusT (interp_ExprA lvar e2) 
+            (interp_ExprA lvar e1))
+ (interp_ExprA lvar e3) (interp_ExprA lvar e1));
+ Rewrite (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1)
+                      (interp_ExprA lvar e3));
+ Rewrite (AplusT_sym (interp_ExprA lvar e1) (interp_ExprA lvar e3));
+ Rewrite <-(AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3)
+                        (interp_ExprA lvar e1));Apply AplusT_sym.
+Unfold assoc;Fold assoc;Unfold interp_ExprA;Fold interp_ExprA;
+ Rewrite assoc_mult_correct;Rewrite (H0 lvar);Simpl;Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Unfold assoc;Fold assoc;Unfold interp_ExprA;Fold interp_ExprA;
+ Rewrite assoc_mult_correct;Simpl;Auto.
+Save.
+
+(**** Distribution *****)
+
+Fixpoint distrib_EAopp [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e2) => (EAplus (distrib_EAopp e1) (distrib_EAopp e2))
+  | (EAmult e1 e2) => (EAmult (distrib_EAopp e1) (distrib_EAopp e2))
+  | (EAopp e) => (EAmult (EAopp EAone) (distrib_EAopp e))
+  | e => e
+  end.
+
+Definition distrib_mult_right :=
+  Fix distrib_mult_right {distrib_mult_right/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAplus t1 t2) =>
+    (EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2))
+  | _ => (EAmult e1 e2)
+  end}.
+
+Definition distrib_mult_left :=
+  Fix distrib_mult_left {distrib_mult_left/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAplus t1 t2) =>
+    (EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2))
+  | _ => (distrib_mult_right e2 e1)
+  end}.
+
+Fixpoint distrib_main [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAmult e1 e2) => (distrib_mult_left (distrib_main e1) (distrib_main e2))
+  | (EAplus e1 e2) => (EAplus (distrib_main e1) (distrib_main e2))
+  | (EAopp e) => (EAopp (distrib_main e))
+  | _ => e
+  end.
+
+Definition distrib [e:ExprA] : ExprA := (distrib_main (distrib_EAopp e)).
+
+Lemma distrib_mult_right_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+     (interp_ExprA lvar (distrib_mult_right e1 e2))==
+     (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)).
+Proof.
+Induction e1;Try Intros;Simpl;Auto.
+Rewrite AmultT_sym;Rewrite AmultT_AplusT_distr;
+ Rewrite (H e2 lvar);Rewrite (H0 e2 lvar);Ring.
+Save.
+
+Lemma distrib_mult_left_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+     (interp_ExprA lvar (distrib_mult_left e1 e2))==
+     (AmultT (interp_ExprA lvar e1)  (interp_ExprA lvar e2)).
+Proof.
+Induction e1;Try Intros;Simpl.
+Rewrite AmultT_Ol;Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_Or.
+Rewrite distrib_mult_right_correct;Simpl;
+ Apply AmultT_sym. 
+Rewrite AmultT_sym;
+ Rewrite (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
+  (interp_ExprA lvar e0)); 
+ Rewrite (AmultT_sym (interp_ExprA lvar e2) (interp_ExprA lvar e));
+ Rewrite (AmultT_sym (interp_ExprA lvar e2) (interp_ExprA lvar e0));
+ Rewrite (H e2 lvar);Rewrite (H0 e2 lvar);Auto.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Save.
+
+Lemma distrib_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (distrib e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Intros;Auto.
+Simpl;Rewrite <- (H lvar);Rewrite <- (H0 lvar); Unfold distrib;Simpl;Auto.
+Simpl;Rewrite <- (H lvar);Rewrite <- (H0 lvar); Unfold distrib;Simpl;
+ Apply distrib_mult_left_correct.
+Simpl;Fold AoppT;Rewrite <- (H lvar);Unfold distrib;Simpl; 
+ Rewrite distrib_mult_right_correct;
+ Simpl;Fold AoppT;Ring.
+Save.
+
+(**** Multiplication by the inverse product ****)
+
+Lemma mult_eq:
+  (e1,e2,a:ExprA)(lvar:(list (Sprod AT nat)))
+    ~((interp_ExprA lvar a)==AzeroT)->
+      (interp_ExprA lvar (EAmult a e1))==(interp_ExprA lvar (EAmult a e2))->
+        (interp_ExprA lvar e1)==(interp_ExprA lvar e2).
+Proof.
+  Simpl;Intros;
+    Apply (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1)
+      (interp_ExprA lvar e2));Assumption.
+Save.
+
+Fixpoint multiply_aux [a,e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e2) =>
+    (EAplus (EAmult a e1) (multiply_aux a e2))
+  | _ => (EAmult a e)
+  end.
+
+Definition multiply [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAmult a e1) => (multiply_aux a e1)
+  | _ => e
+  end.
+
+Lemma multiply_aux_correct:
+  (a,e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (multiply_aux a e))==
+    (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Proof.
+Induction e;Simpl;Intros;Try (Rewrite merge_mult_correct);Auto.
+  Simpl;Rewrite (H0 lvar);Ring.
+Save.
+
+Lemma multiply_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (multiply e))==(interp_ExprA lvar e).
+Proof.
+  Induction e;Simpl;Auto.
+  Intros;Apply multiply_aux_correct.
+Save.
+
+(**** Permutations and simplification ****)
+
+Fixpoint monom_remove [a,m:ExprA] : ExprA :=
+  Cases m of
+  | (EAmult m0 m1) =>
+    (Cases (eqExprA m0 (EAinv a)) of
+     | (left _) => m1
+     | (right _) => (EAmult m0 (monom_remove a m1))
+     end)
+  | _ =>
+    (Cases (eqExprA m (EAinv a)) of
+     | (left _) => EAone
+     | (right _) => (EAmult a m)
+     end)
+  end.
+
+Definition monom_simplif_rem := 
+  Fix monom_simplif_rem {monom_simplif_rem/1:ExprA->ExprA->ExprA:=
+  [a,m:ExprA] 
+  Cases a of
+  | (EAmult a0 a1) => (monom_simplif_rem a1 (monom_remove a0 m))
+  | _ => (monom_remove a m)
+  end}.
+
+Definition monom_simplif [a,m:ExprA] : ExprA :=
+  Cases m of
+  | (EAmult a' m') =>
+    (Cases (eqExprA a a') of
+     | (left _) => (monom_simplif_rem a m')
+     | (right _) => m
+     end)
+  | _ => m
+  end.
+
+Fixpoint inverse_simplif [a,e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e2) => (EAplus (monom_simplif a e1) (inverse_simplif a e2))
+  | _ => (monom_simplif a e)
+  end.
+
+Lemma monom_remove_correct:(e,a:ExprA)
+  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (interp_ExprA lvar (monom_remove a e))==
+  (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Proof.
+Induction e; Intros.
+Simpl;Case (eqExprA EAzero (EAinv a));Intros;[Inversion e0|Simpl;Trivial].
+Simpl;Case (eqExprA EAone (EAinv a));Intros;[Inversion e0|Simpl;Trivial].
+Simpl;Case (eqExprA (EAplus e0 e1) (EAinv a));Intros;[Inversion e2|
+ Simpl;Trivial].
+Simpl;Case (eqExprA e0 (EAinv a));Intros.
+Rewrite e2;Simpl;Fold AinvT.
+Rewrite <-(AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
+             (interp_ExprA lvar e1));
+  Rewrite AinvT_r;[Ring|Assumption].
+Simpl;Rewrite H0;Auto; Ring.
+Simpl;Fold AoppT;Case (eqExprA (EAopp e0) (EAinv a));Intros;[Inversion e1|
+ Simpl;Trivial].
+Unfold monom_remove;Case (eqExprA (EAinv e0) (EAinv a));Intros.
+Case (eqExprA e0 a);Intros.
+Rewrite e2;Simpl;Fold AinvT;Rewrite AinvT_r;Auto.
+Inversion e1;Simpl;ElimType False;Auto.
+Simpl;Trivial.
+Unfold monom_remove;Case (eqExprA (EAvar n) (EAinv a));Intros;
+ [Inversion e0|Simpl;Trivial].
+Save.
+
+Lemma monom_simplif_rem_correct:(a,e:ExprA)
+  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (interp_ExprA lvar (monom_simplif_rem a e))==
+  (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Proof.
+Induction a;Simpl;Intros; Try Rewrite monom_remove_correct;Auto.
+Elim (without_div_O_contr (interp_ExprA lvar e) 
+                          (interp_ExprA lvar e0) H1);Intros.
+Rewrite (H0 (monom_remove e e1) lvar H3);Rewrite monom_remove_correct;Auto.
+Ring.
+Save.
+
+Lemma monom_simplif_correct:(e,a:ExprA)
+  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (interp_ExprA lvar (monom_simplif a e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Intros;Auto.
+Simpl;Case (eqExprA a e0);Intros.
+Rewrite <-e2;Apply monom_simplif_rem_correct;Auto. 
+Simpl;Trivial.
+Save.
+
+Lemma inverse_correct:
+  (e,a:ExprA)(lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+    (interp_ExprA lvar (inverse_simplif a e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Intros;Auto.
+Simpl;Rewrite (H0 a lvar H1); Rewrite monom_simplif_correct ; Auto.
+Unfold inverse_simplif;Rewrite monom_simplif_correct ; Auto.
+Save.
+
+End Theory_of_fields.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
new file mode 100644
index 0000000000..60edfe07d8
--- /dev/null
+++ b/contrib/field/field.ml4
@@ -0,0 +1,113 @@
+(* field.ml4 *)
+
+(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*)
+
+open Names
+open Proof_type
+open Tacinterp
+open Tacmach
+open Term
+open Util
+open Vernacinterp
+
+(* Interpretation of constr's *)
+let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
+
+(* Construction of constants *)
+let constant dir s =
+  let dir = "Coq"::"field"::dir in
+  let id = id_of_string s in
+  try 
+    Declare.global_reference_in_absolute_module dir id
+  with Not_found ->
+    anomaly ("Field: cannot find "^
+	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+
+(* To deal with the optional arguments *)
+let constr_of_opt a opt =
+  let ac = constr_of a in
+  match opt with
+  | None -> mkApp ((constant ["Field_Compl"] "None"),[|ac|])
+  | Some f -> mkApp ((constant ["Field_Compl"] "Some"),[|ac;constr_of f|])
+
+(* Table of theories *)
+let th_tab = ref ((Hashtbl.create 53) : (constr,constr) Hashtbl.t)
+
+let lookup typ = Hashtbl.find !th_tab typ
+
+let _ = 
+  let init () = th_tab := (Hashtbl.create 53) in
+  let freeze () = !th_tab in
+  let unfreeze fs = th_tab := fs in
+  Summary.declare_summary "field"
+    { Summary.freeze_function   = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function     = init;
+      Summary.survive_section   = false }
+
+let load_addfield _ = ()
+let cache_addfield (_,(typ,th)) = Hashtbl.add !th_tab typ th
+let export_addfield x = Some x
+
+(* Declaration of the Add Field library object *)
+let (in_addfield,out_addfield)=
+  Libobject.declare_object
+    ("ADD_FIELD",
+     { Libobject.load_function = load_addfield;
+       Libobject.open_function = cache_addfield;
+       Libobject.cache_function = cache_addfield;
+       Libobject.export_function = export_addfield })
+
+(* Adds a theory to the table *)
+let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
+  ainv_l =
+  begin
+    (try
+       Ring.add_theory true true a aplus amult aone azero aopp aeq rth
+         Quote.ConstrSet.empty
+     with | UserError("Add Semi Ring",_) -> ());
+    let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"),
+      [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
+    Lib.add_anonymous_leaf (in_addfield (a,th))
+  end
+
+(* Vernac command declaration *)
+let _ =
+  let rec opt_arg (aminus_o,adiv_o) = function
+    | (VARG_STRING "minus")::(VARG_CONSTR aminus)::l ->
+      (match aminus_o with
+      |	None -> opt_arg ((Some aminus),adiv_o) l
+      |	_ -> anomaly "AddField")
+    | (VARG_STRING "div")::(VARG_CONSTR adiv)::l ->
+      (match adiv_o with
+      |	None -> opt_arg (aminus_o,(Some adiv)) l
+      |	_ -> anomaly "AddField")
+    | _ -> (aminus_o,adiv_o) in
+  vinterp_add "AddField"
+    (function 
+       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
+	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
+	 ::(VARG_CONSTR aeq)::(VARG_CONSTR ainv)::(VARG_CONSTR rth)
+         ::(VARG_CONSTR ainv_l)::l ->
+         (fun () ->
+           let (aminus_o,adiv_o) = opt_arg (None,None) l in
+           add_field (constr_of a) (constr_of aplus) (constr_of amult)
+             (constr_of aone) (constr_of azero) (constr_of aopp)
+             (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
+             (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l))
+       | _ -> anomaly "AddField")
+
+(* Guesses the type and calls Field_Gen with the right theory *)
+let field g =
+  let evc = project g
+  and env = pf_env g in
+  let typ = constr_of_Constr (interp_tacarg (evc,env,[],[],Some g,get_debug ())
+    <:tactic<
+      Match Context With
+      | [|-(eq ?1 ? ?)] -> ?1
+      |	[|-(eqT ?1 ? ?)] -> ?1>>) in
+  let th = VArg (Constr (lookup typ)) in
+  (tac_interp [("FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
+
+(* Declaration of Field *)
+let _ = hide_tactic "Field" (function _ -> field)
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 0562215feb..8f5779b29c 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -15,6 +15,7 @@
 Require Export Raxioms.
 Require Export ZArithRing.
 Require Omega.
+Require Export Field.
 
 (***************************************************************************)
 (*s       Instantiating Ring tactic on reals                               *)
@@ -37,7 +38,8 @@ Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false).
   Intros; Contradiction.
 Defined.
 
-Add Abstract Ring R Rplus Rmult R1 R0 Ropp [x,y:R]false RTheory.
+Add Field R Rplus Rmult R1 R0 Ropp [x,y:R]false Rinv RTheory Rinv_l
+          with minus:=Rminus div:=Rdiv.
 
 (**************************************************************************)
 (*s  Relation between orders and equality                                 *)