aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-12 08:30:46 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-12 08:30:46 +0000
commit32281da46b561a89b805940cc426563b1b7e6a97 (patch)
treea39376680d89a83d957fac840ed0e1fb3d9b7754 /Makefile
parenta72e2141d8e64774c41bd205753c8c3a3c9c9675 (diff)
Commentaires. Verification des assert false. Probleme des types ML arity.
Correction des dependances pour bin/coq-extraction dans le Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1448 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index ed8faaec4..b6fbb62bf 100644
--- a/Makefile
+++ b/Makefile
@@ -211,7 +211,7 @@ toplevel: $(TOPLEVEL)
EXTRACTIONCMO=contrib/extraction/ocaml.cmo contrib/extraction/extraction.cmo
-bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO)
+bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO) $(EXTRACTIONCMO)
$(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(EXTRACTIONCMO)
###########################################################################