diff options
| author | letouzey | 2001-11-05 17:20:41 +0000 |
|---|---|---|
| committer | letouzey | 2001-11-05 17:20:41 +0000 |
| commit | 8cd83fb8dd41521bbc109d37dd49dd3aae0de373 (patch) | |
| tree | 0292395a354fa041bcfe70976311293994cfe305 /contrib/extraction/test/Makefile | |
| parent | 2e6751cdfb0c25274cf789078438df8579b46f7e (diff) | |
refonte du test
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/Makefile')
| -rw-r--r-- | contrib/extraction/test/Makefile | 29 |
1 files changed, 6 insertions, 23 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index c28e961e9c..af2ae59ffa 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -9,7 +9,7 @@ TOPDIR=../../.. AXIOMSVO:= \ theories/Arith/Arith.vo \ theories/Lists/List.vo \ -theories/Reals/% \ +theories/Reals/Rsyntax.vo \ theories/Num/% \ theories/Relations/Rstar.vo \ theories/Sets/Integers.vo \ @@ -31,7 +31,10 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML)) # General rules # -all: ml $(CMO) v2ml +all: ml theories/Reals/addReals.cmo $(CMO) v2ml + +theories/Reals/addReals.ml: + cp -f addReals theories/Reals/addReals.ml ml: $(ML) @@ -45,33 +48,13 @@ tree: ocamlc $(INCL) -c -i $< $(ML): ml2v - ./extract `./ml2v $@` + ./extract $@ clean: rm -f theories/*/*.ml theories/*/*.cm* theories/*/*.ml.orig # -# Extraction of Reals -# - -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) theories/Reals/addReals.cmo $(REALSCMO) - -realsml: - ./extract_reals $(REALSVO) - -theories/Reals/addReals.ml: - cp -f addReals theories/Reals/addReals.ml - -$(REALSML): realsml - - -# # Utilities # |