diff options
| author | letouzey | 2001-11-07 23:35:13 +0000 |
|---|---|---|
| committer | letouzey | 2001-11-07 23:35:13 +0000 |
| commit | 9e0bd5a13dda8805798fe97a22dce75ac7262302 (patch) | |
| tree | 81b75faae1ffbd4f63ab50089264a4f95fd599d3 /contrib/extraction/test | |
| parent | 90a79b141426a4344df162beb767c48d9b37a765 (diff) | |
Refonte du fichier mlutil.ml. Correction d'un bug d'optim case
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test')
| -rw-r--r-- | contrib/extraction/test/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index af2ae59ffa..9c4f87e944 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -31,7 +31,7 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML)) # General rules # -all: ml theories/Reals/addReals.cmo $(CMO) v2ml +all: v2ml ml theories/Reals/addReals.cmo $(CMO) theories/Reals/addReals.ml: cp -f addReals theories/Reals/addReals.ml @@ -59,7 +59,7 @@ clean: # open: - find theories -name "*".ml -exec qualify2open \{\} \; + find theories -name "*".ml -exec ./qualify2open \{\} \; undo_open: find theories -name "*".ml -exec mv \{\}.orig \{\} \; |