From 90a79b141426a4344df162beb767c48d9b37a765 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 6 Nov 2001 17:55:43 +0000
Subject: suite des tests

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2166 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/test/custom/Adalloc | 4 ++++
 contrib/extraction/test/custom/Fset    | 2 ++
 contrib/extraction/test/custom/Map     | 3 +++
 contrib/extraction/test/custom/Mapcard | 6 ++++++
 contrib/extraction/test/custom/Mapiter | 4 ++++
 contrib/extraction/test/custom/all     | 2 +-
 6 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 contrib/extraction/test/custom/Adalloc
 create mode 100644 contrib/extraction/test/custom/Fset
 create mode 100644 contrib/extraction/test/custom/Map
 create mode 100644 contrib/extraction/test/custom/Mapcard
 create mode 100644 contrib/extraction/test/custom/Mapiter

diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc
new file mode 100644
index 0000000000..f94ba220bf
--- /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 0000000000..c0be70a80a
--- /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 0000000000..7f17c34aa2
--- /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 0000000000..af5c23daa4
--- /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 0000000000..ad4a58735c
--- /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 deeb977d70..4e32680ff9 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.
-- 
cgit v1.2.3