aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2001-03-29 06:38:40 +0000
committerfilliatr2001-03-29 06:38:40 +0000
commit95021d34fd00540b2205f6475a359bdf93a197cb (patch)
tree271fb54c03aa80e38969c64c266ea516375513c4
parent9b3b963a9755fc0d382a9fa3588cd92113ede59d (diff)
fichiers extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1499 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile4
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index cec5b86273..e0c9df0849 100644
--- a/Makefile
+++ b/Makefile
@@ -217,7 +217,9 @@ toplevel: $(TOPLEVEL)
# special binaries for debugging
-EXTRACTIONCMO=contrib/extraction/ocaml.cmo contrib/extraction/extraction.cmo
+EXTRACTIONCMO=contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo \
+ contrib/extraction/extraction.cmo \
+ contrib/extraction/extract_env.cmo
bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO) $(EXTRACTIONCMO)
$(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(EXTRACTIONCMO)