suite des tests

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

6 files changed, 20 insertions, 1 deletions

diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc
new file mode 100644
index 000000000..f94ba220b
--- /dev/null
+++ b/contrib/extraction/test/custom/Adalloc
@@ -0,0 +1,4 @@
+Require Addr.
+Extraction NoInline ad_double ad_double_plus_un.
+Require Map.
+Extraction Inline Map_rec.
diff --git a/contrib/extraction/test/custom/Fset b/contrib/extraction/test/custom/Fset
new file mode 100644
index 000000000..c0be70a80
--- /dev/null
+++ b/contrib/extraction/test/custom/Fset
@@ -0,0 +1,2 @@
+Require Map.
+Extraction Inline Map_rec.
diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map
new file mode 100644
index 000000000..7f17c34aa
--- /dev/null
+++ b/contrib/extraction/test/custom/Map
@@ -0,0 +1,3 @@
+Require Addr.
+Extraction NoInline ad_double ad_double_plus_un.
+
diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard
new file mode 100644
index 000000000..af5c23daa
--- /dev/null
+++ b/contrib/extraction/test/custom/Mapcard
@@ -0,0 +1,6 @@
+Require Plus.
+Extraction NoInline plus_is_one.
+Require Addr.
+Extraction NoInline ad_double ad_double_plus_un.
+Require Map.
+Extraction Inline Map_rec.
diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter
new file mode 100644
index 000000000..ad4a58735
--- /dev/null
+++ b/contrib/extraction/test/custom/Mapiter
@@ -0,0 +1,4 @@
+Require Addr. 
+Extraction NoInline ad_double ad_double_plus_un.
+Require Map.
+Extraction Inline Map_rec.
diff --git a/contrib/extraction/test/custom/all b/contrib/extraction/test/custom/all
index deeb977d7..4e32680ff 100644
--- a/contrib/extraction/test/custom/all
+++ b/contrib/extraction/test/custom/all
@@ -1 +1 @@
-Extraction Inline sigS_rec.
+Extraction Inline sigS_rec prod_rec.