reparation du test des reals

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

7 files changed, 147 insertions, 71 deletions

diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index cb1cf8aa0..edb933104 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -1,11 +1,11 @@
-theories/Arith/compare.cmo: theories/Arith/compare_dec.cmo \
-    theories/Init/specif.cmo 
-theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \
-    theories/Init/specif.cmx 
 theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmo \
     theories/Init/specif.cmo 
 theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \
     theories/Init/specif.cmx 
+theories/Arith/compare.cmo: theories/Arith/compare_dec.cmo \
+    theories/Init/specif.cmo 
+theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \
+    theories/Init/specif.cmx 
 theories/Arith/div2.cmo: theories/Init/datatypes.cmo theories/Init/peano.cmo 
 theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx 
 theories/Arith/eqNat.cmo: theories/Init/datatypes.cmo \
@@ -14,10 +14,10 @@ theories/Arith/eqNat.cmx: theories/Init/datatypes.cmx \
     theories/Init/specif.cmx 
 theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmo \
     theories/Init/datatypes.cmo theories/Arith/minus.cmo \
-    theories/Init/specif.cmo theories/Arith/wf_nat.cmo 
+    theories/Init/specif.cmo 
 theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \
     theories/Init/datatypes.cmx theories/Arith/minus.cmx \
-    theories/Init/specif.cmx theories/Arith/wf_nat.cmx 
+    theories/Init/specif.cmx 
 theories/Arith/even.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
 theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
 theories/Arith/max.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
@@ -34,14 +34,14 @@ theories/Arith/peano_dec.cmx: theories/Init/datatypes.cmx \
     theories/Init/specif.cmx 
 theories/Arith/plus.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
 theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
-theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmo theories/Init/wf.cmo 
-theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx theories/Init/wf.cmx 
-theories/Bool/bool.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
-theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
+theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmo 
+theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx 
 theories/Bool/boolEq.cmo: theories/Init/datatypes.cmo \
     theories/Init/specif.cmo 
 theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \
     theories/Init/specif.cmx 
+theories/Bool/bool.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo 
+theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx 
 theories/Bool/decBool.cmo: theories/Init/specif.cmo 
 theories/Bool/decBool.cmx: theories/Init/specif.cmx 
 theories/Bool/ifProp.cmo: theories/Init/datatypes.cmo \
@@ -61,15 +61,17 @@ theories/Init/specif.cmx: theories/Init/datatypes.cmx
 theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmo \
     theories/IntMap/addr.cmo theories/Init/datatypes.cmo \
     theories/ZArith/fast_integer.cmo theories/IntMap/map.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
 theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \
-    theories/Init/specif.cmx 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
 theories/IntMap/addec.cmo: theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo 
+    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
+    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
 theories/IntMap/addec.cmx: theories/IntMap/addr.cmx \
-    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx 
+    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
 theories/IntMap/addr.cmo: theories/Bool/bool.cmo theories/Init/datatypes.cmo \
     theories/ZArith/fast_integer.cmo theories/Init/specif.cmo 
 theories/IntMap/addr.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \
@@ -81,35 +83,33 @@ theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \
     theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
     theories/Arith/min.cmx 
 theories/IntMap/fset.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/IntMap/map.cmo 
+    theories/Init/datatypes.cmo theories/IntMap/map.cmo \
+    theories/Init/specif.cmo 
 theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
-    theories/Init/datatypes.cmx theories/IntMap/map.cmx 
+    theories/Init/datatypes.cmx theories/IntMap/map.cmx \
+    theories/Init/specif.cmx 
 theories/IntMap/lsort.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
-    theories/IntMap/mapiter.cmo theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo 
+    theories/Bool/bool.cmo theories/Init/datatypes.cmo \
+    theories/ZArith/fast_integer.cmo theories/IntMap/mapiter.cmo \
+    theories/Lists/polyList.cmo theories/Init/specif.cmo \
+    theories/Bool/sumbool.cmo 
 theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
-    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
-    theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx 
-theories/IntMap/map.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
-    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
-    theories/Init/peano.cmo theories/Init/specif.cmo 
-theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
-    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
-    theories/Init/peano.cmx theories/Init/specif.cmx 
+    theories/Bool/bool.cmx theories/Init/datatypes.cmx \
+    theories/ZArith/fast_integer.cmx theories/IntMap/mapiter.cmx \
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Bool/sumbool.cmx 
 theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmo 
 theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx 
 theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmo \
     theories/IntMap/addr.cmo theories/Init/datatypes.cmo \
     theories/IntMap/map.cmo theories/Init/peano.cmo \
     theories/Arith/peano_dec.cmo theories/Arith/plus.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
 theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
     theories/IntMap/map.cmx theories/Init/peano.cmx \
     theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \
-    theories/Init/specif.cmx 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
 theories/IntMap/mapfold.cmo: theories/Init/datatypes.cmo \
     theories/IntMap/fset.cmo theories/IntMap/map.cmo \
     theories/IntMap/mapiter.cmo theories/Init/specif.cmo 
@@ -119,25 +119,31 @@ theories/IntMap/mapfold.cmx: theories/Init/datatypes.cmx \
 theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmo \
     theories/IntMap/addr.cmo theories/Init/datatypes.cmo \
     theories/IntMap/map.cmo theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
 theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
     theories/IntMap/map.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
 theories/IntMap/maplists.cmo: theories/IntMap/addec.cmo \
     theories/Init/datatypes.cmo theories/IntMap/map.cmo \
     theories/IntMap/mapiter.cmo theories/Lists/polyList.cmo \
-    theories/Init/specif.cmo 
+    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
 theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \
     theories/Init/datatypes.cmx theories/IntMap/map.cmx \
     theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx 
-theories/IntMap/mapsubset.cmo: theories/Init/datatypes.cmo \
-    theories/IntMap/fset.cmo theories/IntMap/map.cmo \
-    theories/IntMap/mapiter.cmo 
-theories/IntMap/mapsubset.cmx: theories/Init/datatypes.cmx \
-    theories/IntMap/fset.cmx theories/IntMap/map.cmx \
-    theories/IntMap/mapiter.cmx 
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
+theories/IntMap/map.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \
+    theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \
+    theories/Init/peano.cmo theories/Init/specif.cmo 
+theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
+    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
+    theories/Init/peano.cmx theories/Init/specif.cmx 
+theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmo \
+    theories/Init/datatypes.cmo theories/IntMap/fset.cmo \
+    theories/IntMap/map.cmo theories/IntMap/mapiter.cmo 
+theories/IntMap/mapsubset.cmx: theories/Bool/bool.cmx \
+    theories/Init/datatypes.cmx theories/IntMap/fset.cmx \
+    theories/IntMap/map.cmx theories/IntMap/mapiter.cmx 
 theories/Lists/listSet.cmo: theories/Init/datatypes.cmo \
     theories/Lists/polyList.cmo theories/Init/specif.cmo 
 theories/Lists/listSet.cmx: theories/Init/datatypes.cmx \
@@ -156,30 +162,40 @@ theories/Reals/addReals.cmo: theories/ZArith/fast_integer.cmo \
     theories/Reals/typeSyntax.cmo 
 theories/Reals/addReals.cmx: theories/ZArith/fast_integer.cmx \
     theories/Reals/typeSyntax.cmx 
-theories/Reals/r_Ifp.cmo: theories/Reals/addReals.cmo \
-    theories/ZArith/fast_integer.cmo theories/Reals/raxioms.cmo \
-    theories/Reals/rdefinitions.cmo theories/ZArith/zarith_aux.cmo 
-theories/Reals/r_Ifp.cmx: theories/Reals/addReals.cmx \
-    theories/ZArith/fast_integer.cmx theories/Reals/raxioms.cmx \
-    theories/Reals/rdefinitions.cmx theories/ZArith/zarith_aux.cmx 
+theories/Reals/ranalysis.cmo: theories/Reals/rdefinitions.cmo 
+theories/Reals/ranalysis.cmx: theories/Reals/rdefinitions.cmx 
 theories/Reals/raxioms.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo 
+    theories/ZArith/fast_integer.cmo theories/Reals/rdefinitions.cmo 
 theories/Reals/raxioms.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx 
+    theories/ZArith/fast_integer.cmx theories/Reals/rdefinitions.cmx 
 theories/Reals/rbase.cmo: theories/Reals/addReals.cmo \
-    theories/Reals/typeSyntax.cmo theories/ZArith/zarith_aux.cmo 
+    theories/Init/datatypes.cmo theories/Reals/raxioms.cmo \
+    theories/Reals/rdefinitions.cmo theories/Reals/typeSyntax.cmo \
+    theories/ZArith/zarith_aux.cmo 
 theories/Reals/rbase.cmx: theories/Reals/addReals.cmx \
-    theories/Reals/typeSyntax.cmx theories/ZArith/zarith_aux.cmx 
+    theories/Init/datatypes.cmx theories/Reals/raxioms.cmx \
+    theories/Reals/rdefinitions.cmx theories/Reals/typeSyntax.cmx \
+    theories/ZArith/zarith_aux.cmx 
 theories/Reals/rbasic_fun.cmo: theories/Reals/rbase.cmo \
-    theories/Reals/typeSyntax.cmo 
+    theories/Reals/rdefinitions.cmo theories/Reals/typeSyntax.cmo 
 theories/Reals/rbasic_fun.cmx: theories/Reals/rbase.cmx \
-    theories/Reals/typeSyntax.cmx 
+    theories/Reals/rdefinitions.cmx theories/Reals/typeSyntax.cmx 
 theories/Reals/rfunctions.cmo: theories/Init/datatypes.cmo \
     theories/ZArith/fast_integer.cmo theories/Arith/minus.cmo \
-    theories/Init/peano.cmo 
+    theories/Init/peano.cmo theories/Reals/rdefinitions.cmo 
 theories/Reals/rfunctions.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Arith/minus.cmx \
-    theories/Init/peano.cmx 
+    theories/Init/peano.cmx theories/Reals/rdefinitions.cmx 
+theories/Reals/rgeom.cmo: theories/Reals/r_sqr.cmo theories/Reals/rbase.cmo \
+    theories/Reals/rdefinitions.cmo theories/Reals/rtrigo.cmo 
+theories/Reals/rgeom.cmx: theories/Reals/r_sqr.cmx theories/Reals/rbase.cmx \
+    theories/Reals/rdefinitions.cmx theories/Reals/rtrigo.cmx 
+theories/Reals/r_Ifp.cmo: theories/Reals/addReals.cmo \
+    theories/ZArith/fast_integer.cmo theories/Reals/raxioms.cmo \
+    theories/Reals/rdefinitions.cmo theories/ZArith/zarith_aux.cmo 
+theories/Reals/r_Ifp.cmx: theories/Reals/addReals.cmx \
+    theories/ZArith/fast_integer.cmx theories/Reals/raxioms.cmx \
+    theories/Reals/rdefinitions.cmx theories/ZArith/zarith_aux.cmx 
 theories/Reals/rlimit.cmo: theories/Reals/rbasic_fun.cmo \
     theories/Reals/rdefinitions.cmo 
 theories/Reals/rlimit.cmx: theories/Reals/rbasic_fun.cmx \
@@ -188,6 +204,22 @@ theories/Reals/rseries.cmo: theories/Init/datatypes.cmo \
     theories/Reals/rbasic_fun.cmo 
 theories/Reals/rseries.cmx: theories/Init/datatypes.cmx \
     theories/Reals/rbasic_fun.cmx 
+theories/Reals/rsigma.cmo: theories/Init/datatypes.cmo \
+    theories/Reals/rdefinitions.cmo 
+theories/Reals/rsigma.cmx: theories/Init/datatypes.cmx \
+    theories/Reals/rdefinitions.cmx 
+theories/Reals/r_sqr.cmo: theories/Reals/rbase.cmo \
+    theories/Reals/rdefinitions.cmo 
+theories/Reals/r_sqr.cmx: theories/Reals/rbase.cmx \
+    theories/Reals/rdefinitions.cmx 
+theories/Reals/rtrigo.cmo: theories/Init/datatypes.cmo \
+    theories/Init/peano.cmo theories/Reals/raxioms.cmo \
+    theories/Reals/rdefinitions.cmo theories/Reals/rfunctions.cmo \
+    theories/Reals/rsigma.cmo 
+theories/Reals/rtrigo.cmx: theories/Init/datatypes.cmx \
+    theories/Init/peano.cmx theories/Reals/raxioms.cmx \
+    theories/Reals/rdefinitions.cmx theories/Reals/rfunctions.cmx \
+    theories/Reals/rsigma.cmx 
 theories/Relations/relation_Operators.cmo: theories/Lists/polyList.cmo \
     theories/Init/specif.cmo 
 theories/Relations/relation_Operators.cmx: theories/Lists/polyList.cmx \
@@ -222,27 +254,45 @@ theories/Sorting/sorting.cmo: theories/Lists/polyList.cmo \
     theories/Init/specif.cmo 
 theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \
     theories/Init/specif.cmx 
-theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmo \
-    theories/Init/wf.cmo 
-theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx \
-    theories/Init/wf.cmx 
+theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmo 
+theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx 
 theories/ZArith/fast_integer.cmo: theories/Init/datatypes.cmo \
     theories/Init/peano.cmo 
 theories/ZArith/fast_integer.cmx: theories/Init/datatypes.cmx \
     theories/Init/peano.cmx 
 theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo theories/Init/peano.cmo 
+    theories/ZArith/fast_integer.cmo theories/Init/peano.cmo \
+    theories/ZArith/zarith_aux.cmo 
 theories/ZArith/wf_Z.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/Init/peano.cmx 
-theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmo \
-    theories/Init/specif.cmo 
-theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \
-    theories/Init/specif.cmx 
+    theories/ZArith/fast_integer.cmx theories/Init/peano.cmx \
+    theories/ZArith/zarith_aux.cmx 
 theories/ZArith/zarith_aux.cmo: theories/Init/datatypes.cmo \
-    theories/ZArith/fast_integer.cmo 
+    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo 
 theories/ZArith/zarith_aux.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx 
+    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx 
+theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmo \
+    theories/Init/specif.cmo theories/Bool/sumbool.cmo 
+theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \
+    theories/Init/specif.cmx theories/Bool/sumbool.cmx 
+theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmo \
+    theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \
+    theories/ZArith/wf_Z.cmo theories/ZArith/zArith_dec.cmo \
+    theories/ZArith/zarith_aux.cmo 
+theories/ZArith/zcomplements.cmx: theories/Init/datatypes.cmx \
+    theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
+    theories/ZArith/wf_Z.cmx theories/ZArith/zArith_dec.cmx \
+    theories/ZArith/zarith_aux.cmx 
+theories/ZArith/zlogarithm.cmo: theories/ZArith/fast_integer.cmo \
+    theories/ZArith/zarith_aux.cmo 
+theories/ZArith/zlogarithm.cmx: theories/ZArith/fast_integer.cmx \
+    theories/ZArith/zarith_aux.cmx 
 theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmo \
     theories/ZArith/fast_integer.cmo theories/Init/specif.cmo 
 theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Init/specif.cmx 
+theories/ZArith/zpower.cmo: theories/Init/datatypes.cmo \
+    theories/ZArith/fast_integer.cmo theories/ZArith/zarith_aux.cmo \
+    theories/ZArith/zmisc.cmo 
+theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \
+    theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \
+    theories/ZArith/zmisc.cmx 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 82bbb1d3f..844b71a57 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -30,13 +30,8 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML))
 #	General rules 
 #
 
-#all: v2ml ml theories/Reals/addReals.cmo $(CMO)
-
 all: v2ml ml $(CMO)
 
-theories/Reals/addReals.ml: 
-	cp -f addReals theories/Reals/addReals.ml
-
 ml: $(ML)
 
 depend: $(ML)
@@ -72,6 +67,28 @@ v2ml: v2ml.ml
 	ocamlc -o $@ $< 
 	$(MAKE)
 
+#
+#	Extraction of Reals
+#
+
+
+REALSAXIOMSVO:=theories/Reals/Rsyntax.vo
+
+REALSALLVO:=$(shell cd $(TOPDIR); ls -tr theories/Reals/*.vo)
+REALSVO:=$(filter-out $(REALSAXIOMSVO),$(REALSALLVO))
+REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO))
+REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
+
+reals: all realsml theories/Reals/addReals.cmo $(REALSCMO)
+
+realsml: $(REALSML)
+
+theories/Reals/addReals.ml: 
+	cp -f addReals theories/Reals/addReals.ml
+
+$(REALSML): 
+	./extract $@
+
 
 #
 #	The End
diff --git a/contrib/extraction/test/custom/R_sqr b/contrib/extraction/test/custom/R_sqr
new file mode 100644
index 000000000..d8f1b3e7b
--- /dev/null
+++ b/contrib/extraction/test/custom/R_sqr
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Ranalysis b/contrib/extraction/test/custom/Ranalysis
new file mode 100644
index 000000000..d8f1b3e7b
--- /dev/null
+++ b/contrib/extraction/test/custom/Ranalysis
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v
index b817c3600..ed8dc1084 100644
--- a/contrib/extraction/test/custom/Reals.v
+++ b/contrib/extraction/test/custom/Reals.v
@@ -14,3 +14,4 @@ Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))"
 Extract Inlined Constant PI => "3.141593".
 Extract Inlined Constant cos => cos.
 Extract Inlined Constant sin => sin.
+Extract Inlined Constant derive_pt => "(fun f x -> ((f (x+.1E-5))-.(f x))*.1E5)".
diff --git a/contrib/extraction/test/custom/Rgeom b/contrib/extraction/test/custom/Rgeom
new file mode 100644
index 000000000..d8f1b3e7b
--- /dev/null
+++ b/contrib/extraction/test/custom/Rgeom
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rtrigo b/contrib/extraction/test/custom/Rtrigo
new file mode 100644
index 000000000..d8f1b3e7b
--- /dev/null
+++ b/contrib/extraction/test/custom/Rtrigo
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+