diff options
| author | letouzey | 2001-09-20 14:14:35 +0000 |
|---|---|---|
| committer | letouzey | 2001-09-20 14:14:35 +0000 |
| commit | d9acd0a5dc55d422e18e8caf318dc325c16c2535 (patch) | |
| tree | 1c9ad88431a71418fd352ec23532c22b0c5e2651 | |
| parent | 5072976c16bcb2e3c4d4116d63d949562ad0085c (diff) | |
changements mineurs du test
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2020 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/test/.depend | 22 | ||||
| -rw-r--r-- | contrib/extraction/test/Makefile | 6 | ||||
| -rw-r--r-- | contrib/extraction/test/addReals (renamed from contrib/extraction/test/addReals.ml) | 0 |
3 files changed, 16 insertions, 12 deletions
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index a01546554f..89ca9205c2 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -160,20 +160,22 @@ theories/Reals/addReals.cmo: theories/ZArith/fast_integer.cmo \ theories/Reals/typeSyntax.cmo theories/Reals/addReals.cmx: theories/ZArith/fast_integer.cmx \ theories/Reals/typeSyntax.cmx -theories/Reals/r_Ifp.cmo: addReals.cmo theories/ZArith/fast_integer.cmo \ - theories/Reals/raxioms.cmo theories/Reals/rdefinitions.cmo \ - theories/ZArith/zarith_aux.cmo -theories/Reals/r_Ifp.cmx: addReals.cmx theories/ZArith/fast_integer.cmx \ - theories/Reals/raxioms.cmx theories/Reals/rdefinitions.cmx \ - theories/ZArith/zarith_aux.cmx +theories/Reals/r_Ifp.cmo: theories/Reals/addReals.cmo \ + theories/ZArith/fast_integer.cmo theories/Reals/raxioms.cmo \ + theories/Reals/rdefinitions.cmo theories/ZArith/zarith_aux.cmo +theories/Reals/r_Ifp.cmx: theories/Reals/addReals.cmx \ + theories/ZArith/fast_integer.cmx theories/Reals/raxioms.cmx \ + theories/Reals/rdefinitions.cmx theories/ZArith/zarith_aux.cmx theories/Reals/raxioms.cmo: theories/Init/datatypes.cmo \ theories/ZArith/fast_integer.cmo theories/Reals/raxioms.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx -theories/Reals/rbase.cmo: addReals.cmo theories/Init/specif.cmo \ - theories/Reals/typeSyntax.cmo theories/ZArith/zarith_aux.cmo -theories/Reals/rbase.cmx: addReals.cmx theories/Init/specif.cmx \ - theories/Reals/typeSyntax.cmx theories/ZArith/zarith_aux.cmx +theories/Reals/rbase.cmo: theories/Reals/addReals.cmo \ + theories/Init/specif.cmo theories/Reals/typeSyntax.cmo \ + theories/ZArith/zarith_aux.cmo +theories/Reals/rbase.cmx: theories/Reals/addReals.cmx \ + theories/Init/specif.cmx theories/Reals/typeSyntax.cmx \ + theories/ZArith/zarith_aux.cmx theories/Reals/rbasic_fun.cmo: theories/Reals/rbase.cmo \ theories/Reals/typeSyntax.cmo theories/Reals/rbasic_fun.cmx: theories/Reals/rbase.cmx \ diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index fd37b46872..e3e44e0513 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -31,7 +31,7 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML)) # General rules # -all: $(ML) depend $(CMO) v2ml +all: $(ML) $(CMO) v2ml depend: $(ML) rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend @@ -62,7 +62,9 @@ reals: all $(REALSML) theories/Reals/addReals.cmo $(REALSCMO) realsml: ./extract_reals $(REALSVO) - cp -f addReals.ml theories/Reals + +theories/Reals/addReals.ml: + cp -f addReals theories/Reals/addReals.ml $(REALSML): realsml diff --git a/contrib/extraction/test/addReals.ml b/contrib/extraction/test/addReals index 86e9a79947..86e9a79947 100644 --- a/contrib/extraction/test/addReals.ml +++ b/contrib/extraction/test/addReals |