diff options
Diffstat (limited to 'tools/coq_makefile.ml4')
-rw-r--r-- | tools/coq_makefile.ml4 | 3 |
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; |