diff options
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 $@ |