refonte du test

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

13 files changed, 32 insertions, 0 deletions

diff --git a/contrib/extraction/test/custom/ListSet b/contrib/extraction/test/custom/ListSet
new file mode 100644
index 0000000000..c9bea52a4c
--- /dev/null
+++ b/contrib/extraction/test/custom/ListSet
@@ -0,0 +1 @@
+Extraction NoInline set_add set_mem.
diff --git a/contrib/extraction/test/custom/PolyList b/contrib/extraction/test/custom/PolyList
new file mode 100644
index 0000000000..ffee7dc9c1
--- /dev/null
+++ b/contrib/extraction/test/custom/PolyList
@@ -0,0 +1 @@
+Extraction NoInline map.
diff --git a/contrib/extraction/test/custom/R_Ifp b/contrib/extraction/test/custom/R_Ifp
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/R_Ifp
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Raxioms b/contrib/extraction/test/custom/Raxioms
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Raxioms
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rbase b/contrib/extraction/test/custom/Rbase
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rbase
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rbasic_fun b/contrib/extraction/test/custom/Rbasic_fun
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rbasic_fun
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rdefinitions b/contrib/extraction/test/custom/Rdefinitions
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rdefinitions
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v
new file mode 100644
index 0000000000..d42fe0a53c
--- /dev/null
+++ b/contrib/extraction/test/custom/Reals.v
@@ -0,0 +1,12 @@
+Require Reals. 
+Extract Inlined Constant R => float.
+Extract Inlined Constant R0 => "0.0".
+Extract Inlined Constant R1 => "1.0".
+Extract Inlined Constant Rplus => "(+.)".
+Extract Inlined Constant Rmult => "( *.)".
+Extract Inlined Constant Ropp => "(~-.)".
+Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)".
+Extract Inlined Constant Rlt => "(<)".
+Extract Inlined Constant up => "AddReals.my_ceil".
+Extract Inlined Constant total_order_T => "AddReals.total_order_T".
+
diff --git a/contrib/extraction/test/custom/Rfunctions b/contrib/extraction/test/custom/Rfunctions
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rfunctions
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rlimit b/contrib/extraction/test/custom/Rlimit
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rlimit
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/Rseries b/contrib/extraction/test/custom/Rseries
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Rseries
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+
diff --git a/contrib/extraction/test/custom/all b/contrib/extraction/test/custom/all
new file mode 100644
index 0000000000..deeb977d70
--- /dev/null
+++ b/contrib/extraction/test/custom/all
@@ -0,0 +1 @@
+Extraction Inline sigS_rec.
diff --git a/contrib/extraction/test/custom/fast_integer b/contrib/extraction/test/custom/fast_integer
new file mode 100644
index 0000000000..e2b2495340
--- /dev/null
+++ b/contrib/extraction/test/custom/fast_integer
@@ -0,0 +1 @@
+Extraction NoInline Zero_suivi_de Un_suivi_de.