Ajout Fourier, DiscrR, ...

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

3 files changed, 64 insertions, 17 deletions

diff --git a/.depend b/.depend
index 13b4364e1c..247a565b56 100644
--- a/.depend
+++ b/.depend
@@ -1162,18 +1162,18 @@ toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
     kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \
     proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
-    kernel/reduction.cmi library/states.cmi pretyping/syntax_def.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi \
-    toplevel/command.cmi 
+    kernel/reduction.cmi kernel/safe_typing.cmi library/states.cmi \
+    pretyping/syntax_def.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/command.cmi 
 toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
     kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
     kernel/evd.cmx library/global.cmx library/impargs.cmx library/indrec.cmx \
     kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \
     proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
-    kernel/reduction.cmx library/states.cmx pretyping/syntax_def.cmx \
-    proofs/tacmach.cmx pretyping/tacred.cmx kernel/term.cmx lib/util.cmx \
-    toplevel/command.cmi 
+    kernel/reduction.cmx kernel/safe_typing.cmx library/states.cmx \
+    pretyping/syntax_def.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/command.cmi 
 toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \
     toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi 
@@ -1596,14 +1596,14 @@ contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi library/global.cmi lib/gmap.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
-    contrib/extraction/extraction.cmi 
+    kernel/reduction.cmi library/summary.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi contrib/extraction/extraction.cmi 
 contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
     kernel/environ.cmx kernel/evd.cmx library/global.cmx lib/gmap.cmx \
     kernel/inductive.cmx kernel/instantiate.cmx contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmx kernel/names.cmx lib/pp.cmx \
-    kernel/reduction.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
-    contrib/extraction/extraction.cmi 
+    kernel/reduction.cmx library/summary.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx contrib/extraction/extraction.cmi 
 contrib/extraction/mlutil.cmo: kernel/declarations.cmi library/global.cmi \
     library/lib.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
     kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
@@ -1634,6 +1634,16 @@ contrib/field/field.cmx: parsing/astterm.cmx parsing/coqast.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/fourier/fourierR.cmo: parsing/astterm.cmi proofs/clenv.cmi \
+    tactics/equality.cmi kernel/evd.cmi contrib/fourier/fourier.cmo \
+    library/global.cmi kernel/names.cmi parsing/pcoq.cmi \
+    contrib/ring/ring.cmo proofs/tacmach.cmi tactics/tactics.cmi \
+    kernel/term.cmi 
+contrib/fourier/fourierR.cmx: parsing/astterm.cmx proofs/clenv.cmx \
+    tactics/equality.cmx kernel/evd.cmx contrib/fourier/fourier.cmx \
+    library/global.cmx kernel/names.cmx parsing/pcoq.cmx \
+    contrib/ring/ring.cmx proofs/tacmach.cmx tactics/tactics.cmx \
+    kernel/term.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 \
diff --git a/.depend.coq b/.depend.coq
index f64efe6a94..47db4e775f 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -44,8 +44,9 @@ theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definiti
 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/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
 theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo
+theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.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
@@ -54,6 +55,7 @@ theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.v
 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/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
 theories/Num/SubProps.vo: theories/Num/SubProps.v
 theories/Num/Params.vo: theories/Num/Params.v
 theories/Num/OppProps.vo: theories/Num/OppProps.v
@@ -150,9 +152,23 @@ 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/Fourier.vo: test-suite/success/Fourier.v theories/Reals/SplitAbsolu.vo contrib/fourier/Fourier.vo
+test-suite/success/Field.vo: test-suite/success/Field.v theories/Reals/Reals.vo
+test-suite/success/DiscrR.vo: test-suite/success/DiscrR.v theories/Reals/Reals.vo theories/Reals/DiscrR.vo
 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/CasesDep.vo: test-suite/success/CasesDep.v theories/Init/Prelude.vo theories/Init/Logic_TypeSyntax.vo theories/Init/Logic_Type.vo
+test-suite/success/Cases.vo: test-suite/success/Cases.v theories/Bool/Bool.vo theories/Arith/Peano_dec.vo theories/Arith/Arith.vo theories/ZArith/ZArith.vo
+test-suite/success/Case9.vo: test-suite/success/Case9.v
+test-suite/success/Case8.vo: test-suite/success/Case8.v
+test-suite/success/Case7.vo: test-suite/success/Case7.v
+test-suite/success/Case6.vo: test-suite/success/Case6.v
+test-suite/success/Case5.vo: test-suite/success/Case5.v
+test-suite/success/Case4.vo: test-suite/success/Case4.v
+test-suite/success/Case3.vo: test-suite/success/Case3.v
+test-suite/success/Case2.vo: test-suite/success/Case2.v
+test-suite/success/Case10.vo: test-suite/success/Case10.v
+test-suite/success/Case1.vo: test-suite/success/Case1.v
 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
@@ -163,6 +179,20 @@ 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/failure/Case9.vo: test-suite/failure/Case9.v
+test-suite/failure/Case8.vo: test-suite/failure/Case8.v
+test-suite/failure/Case7.vo: test-suite/failure/Case7.v
+test-suite/failure/Case6.vo: test-suite/failure/Case6.v
+test-suite/failure/Case5.vo: test-suite/failure/Case5.v
+test-suite/failure/Case4.vo: test-suite/failure/Case4.v
+test-suite/failure/Case3.vo: test-suite/failure/Case3.v
+test-suite/failure/Case2.vo: test-suite/failure/Case2.v
+test-suite/failure/Case14.vo: test-suite/failure/Case14.v
+test-suite/failure/Case13.vo: test-suite/failure/Case13.v
+test-suite/failure/Case12.vo: test-suite/failure/Case12.v
+test-suite/failure/Case11.vo: test-suite/failure/Case11.v
+test-suite/failure/Case10.vo: test-suite/failure/Case10.v
+test-suite/failure/Case1.vo: test-suite/failure/Case1.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
 contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
@@ -180,8 +210,10 @@ 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/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/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/fourier/Fourier_util.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_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.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
@@ -194,7 +226,6 @@ contrib/correctness/ProgramsExtraction.vo: contrib/correctness/ProgramsExtractio
 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/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/Arrays_stuff.vo: contrib/correctness/Arrays_stuff.v contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo contrib/correctness/Sorted.vo
diff --git a/Makefile b/Makefile
index 1102f670c4..55b841dfc3 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
               -I proofs -I tactics -I pretyping -I parsing -I toplevel  \
               -I contrib/omega -I contrib/ring -I contrib/xml \
 	      -I contrib/extraction -I contrib/correctness \
-              -I contrib/interface
+              -I contrib/interface -I contrib/fourier
 
 INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
@@ -197,6 +197,7 @@ CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.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 \
+	contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \
 	$(EXTRACTIONCMO) $(CORRECTNESSCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
@@ -406,7 +407,8 @@ WELLFOUNDEDVO=theories/Wellfounded/Disjoint_Union.vo \
 REALSVO=theories/Reals/TypeSyntax.vo \
 	theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \
 	theories/Reals/Raxioms.vo      theories/Reals/Rbase.vo \
-	theories/Reals/R_Ifp.vo        theories/Reals/Rbasic_fun.vo \
+	theories/Reals/DiscrR.vo       theories/Reals/R_Ifp.vo \
+	theories/Reals/Rbasic_fun.vo   theories/Reals/SplitAbsolu.vo \
 	theories/Reals/Rfunctions.vo   theories/Reals/Rlimit.vo \
 	theories/Reals/Rderiv.vo       theories/Reals/Reals.vo 
 
@@ -462,6 +464,8 @@ XMLVO = contrib/xml/Xml.vo
 
 INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc
 
+FOURIERVO = contrib/fourier/Fourier_util.vo    contrib/fourier/Fourier.vo
+
 contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
 	$(COQC) -boot -byte  $(COQINCLUDES) $<
 
@@ -469,7 +473,7 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init
 	$(COQC) -boot -byte  $(COQINCLUDES) $<
 
 CONTRIBVO = $(OMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\
-            $(INTERFACEV0)
+            $(INTERFACEV0) $(FOURIERVO)
 
 $(CONTRIBVO): states/initial.coq
 
@@ -479,6 +483,8 @@ ring: $(RINGVO)
 xml: $(XMLVO)
 extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
 correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
+field: $(FIELDVO)
+fourier: $(FOURIERVO)
 
 clean::
 	rm -f contrib/*/*.cm[io] contrib/*/*.vo