aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_makefile.ml4')
-rw-r--r--tools/coq_makefile.ml43
1 files changed, 1 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index aec2f82f9..42fe0b0a1 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -191,8 +191,7 @@ let variables l =
print "CAMLOPTLINK=ocamlopt\n";
print "COQDEP=$(COQBIN)coqdep -c\n";
print "COQVO2XML=coq_vo2xml\n";
- print "GRAMMARS=grammar.cma g_constr.cmo g_tactic.cmo g_ltac.cmo \\
- g_basevernac.cmo tacextend.cmo vernacextend.cmo\n";
+ print "GRAMMARS=grammar.cma";
print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
var_aux l;