diff options
| author | letouzey | 2004-03-20 17:39:10 +0000 |
|---|---|---|
| committer | letouzey | 2004-03-20 17:39:10 +0000 |
| commit | fa6eb2b27f08efff4013fe559abbdea5575675f8 (patch) | |
| tree | 4ab2d2b67f161a678d29a13921ea67697a20e26a /contrib/extraction/test/Makefile | |
| parent | bb13436bfd602c8b03466339241d4e8491074e71 (diff) | |
petit rajeunissement du test d'extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/Makefile')
| -rw-r--r-- | contrib/extraction/test/Makefile | 13 |
1 files changed, 6 insertions, 7 deletions
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 $@ |