From fa6eb2b27f08efff4013fe559abbdea5575675f8 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 20 Mar 2004 17:39:10 +0000
Subject: petit rajeunissement du test d'extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5538 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/test/Makefile | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'contrib/extraction/test/Makefile')

diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 4ab5fe7fb7..c9bb56237c 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -7,12 +7,8 @@ TOPDIR=../../..
 # Files with axioms to be realized: can't be extracted directly
 
 AXIOMSVO:= \
-theories/Arith/Arith.vo \
-theories/Lists/List.vo \
 theories/Reals/% \
-theories/Reals/Rsyntax.vo \
-theories/Num/% \
-theories/ZArith/Zsyntax.vo
+theories/Num/%
 
 DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
 
@@ -28,6 +24,8 @@ MLI:= $(patsubst %.ml,%.mli,$(ML))
 
 CMO:= $(patsubst %.ml,%.cmo,$(ML))
 
+OSTDLIB:=$(shell (ocamlc -where))
+
 #
 #	General rules 
 #
@@ -41,15 +39,16 @@ depend: $(ML)
 
 tree:
 	mkdir -p $(DIRS)
+	cp $(OSTDLIB)/pervasives.cmi $(OSTDLIB)/obj.cmi $(OSTDLIB)/lazy.cmi theories
 
 #%.mli:%.ml
 #	./make_mli $< > $@
 
 %.cmi:%.mli
-	ocamlc $(INCL) -c -i $<
+	ocamlc -c $(INCL) -nostdlib $<
 
 %.cmo:%.ml
-	ocamlc $(INCL) -c -i $<
+	ocamlc -c $(INCL) -nostdlib $<
 
 $(ML): ml2v
 	./extract $@
-- 
cgit v1.2.3