From 7bdde88e133bb78c4ca6f6bd15e49131fbaf0063 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 25 Apr 2001 08:10:23 +0000
Subject: make reals prend en compte tous les .vo de theories/Reals

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1712 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/test/.cvsignore    |  1 -
 contrib/extraction/test/Makefile      | 16 ++++------------
 contrib/extraction/test/extract_reals | 16 ++++++----------
 3 files changed, 10 insertions(+), 23 deletions(-)

(limited to 'contrib/extraction/test')

diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore
index e230de3cf..042418cd3 100644
--- a/contrib/extraction/test/.cvsignore
+++ b/contrib/extraction/test/.cvsignore
@@ -1,6 +1,5 @@
 theories
 ml2v 
 v2ml
-.depend
 log
 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 957cddcf2..d6d20f0c2 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -53,23 +53,15 @@ clean:
 #	Extraction of Reals
 #
 
-REALSML:= \
-theories/Reals/typeSyntax.ml \
-theories/Reals/addReals.ml \
-theories/Reals/rdefinitions.ml \
-theories/Reals/raxioms.ml \
-theories/Reals/r_Ifp.ml \
-theories/Reals/rbase.ml \
-theories/Reals/rbasic_fun.ml \
-theories/Reals/rlimit.ml \
-theories/Reals/rderiv.ml
-
+REALSALLVO:=$(shell cd ../../..; ls -tr theories/Reals/*.vo)
+REALSVO:=$(filter-out theories/Reals/Rsyntax.vo,$(REALSALLVO))
+REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO))
 REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML))
 
 reals: all $(REALSML) $(REALSCMO)
 
 realsml: 
-	./extract_reals
+	./extract_reals $(REALSVO)
 	cp -f addReals.ml theories/Reals
 
 $(REALSML): realsml
diff --git a/contrib/extraction/test/extract_reals b/contrib/extraction/test/extract_reals
index 92749ff0a..4d15cc4e8 100755
--- a/contrib/extraction/test/extract_reals
+++ b/contrib/extraction/test/extract_reals
@@ -13,19 +13,15 @@ Extract Constant Rinv => "(fun x -> 1.0 /. x)".
 Extract Constant Rlt => "(<)".
 Extract Constant up => "AddReals.my_ceil".
 Extract Constant total_order_T => "AddReals.total_order_T".
-Extraction Module Rdefinitions.
-Extraction Module TypeSyntax.
-Extraction Module Raxioms.
-Extraction Module Rbase.   
-Extraction Module R_Ifp.
-Extraction Module Rbasic_fun.
-Extraction Module Rlimit.
-Extraction Module Rfunctions.
-Extraction Module Rderiv.
 EOF
+for f in $*; do
+    ff=`basename $f .vo`
+    echo "Require $ff." >> /tmp/extr$$.v
+    echo "Extraction Module $ff." >> /tmp/extr$$.v
+done
 ../../../bin/coqtop.opt -silent -batch -load-vernac-source /tmp/extr$$.v
 out=$?
-rm -f /tmp/extr$$.v
+#rm -f /tmp/extr$$.v
 exit $out
 
 
-- 
cgit v1.2.3