diff options
| author | letouzey | 2002-03-21 17:06:15 +0000 |
|---|---|---|
| committer | letouzey | 2002-03-21 17:06:15 +0000 |
| commit | 88ff300b20833b71ec5d31fffcc766dda9aba365 (patch) | |
| tree | a45d404db9d74762f3b21e46485ec498b26695b8 /contrib/extraction/test/Makefile | |
| parent | 04117381b1130ed2cde716c7b80f34e625b9b276 (diff) | |
reparation du test des reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/Makefile')
| -rw-r--r-- | contrib/extraction/test/Makefile | 27 |
1 files changed, 22 insertions, 5 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 82bbb1d3f3..844b71a57d 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -30,13 +30,8 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML)) # General rules # -#all: v2ml ml theories/Reals/addReals.cmo $(CMO) - all: v2ml ml $(CMO) -theories/Reals/addReals.ml: - cp -f addReals theories/Reals/addReals.ml - ml: $(ML) depend: $(ML) @@ -72,6 +67,28 @@ v2ml: v2ml.ml ocamlc -o $@ $< $(MAKE) +# +# Extraction of Reals +# + + +REALSAXIOMSVO:=theories/Reals/Rsyntax.vo + +REALSALLVO:=$(shell cd $(TOPDIR); ls -tr theories/Reals/*.vo) +REALSVO:=$(filter-out $(REALSAXIOMSVO),$(REALSALLVO)) +REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO)) +REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML)) + +reals: all realsml theories/Reals/addReals.cmo $(REALSCMO) + +realsml: $(REALSML) + +theories/Reals/addReals.ml: + cp -f addReals theories/Reals/addReals.ml + +$(REALSML): + ./extract $@ + # # The End |