summaryrefslogtreecommitdiff
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml26
1 files changed, 14 insertions, 12 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index a685d6ea..20117ca6 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -315,10 +315,10 @@ in
print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.g: %.v\n\t$(GALLINA) $<\n\n";
- print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n";
- print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n";
- print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
- print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n";
+ print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
+ print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
+ print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
+ print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@\n\n";
print "%.v.d: %.v\n";
print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
@@ -349,11 +349,13 @@ let variables is_install opt (args,defs) =
print "\n";
end;
(* Coq executables and relative variables *)
+ if !some_vfile || !some_mlpackfile || !some_mllibfile then
+ print "COQDEP?=$(COQBIN)coqdep -c\n";
if !some_vfile then begin
print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
print "COQCHKFLAGS?=-silent -o\n";
+ print "COQDOCFLAGS?=-interpolate -utf8\n";
print "COQC?=$(COQBIN)coqc\n";
- print "COQDEP?=$(COQBIN)coqdep -c\n";
print "GALLINA?=$(COQBIN)gallina\n";
print "COQDOC?=$(COQBIN)coqdoc\n";
print "COQCHK?=$(COQBIN)coqchk\n\n";
@@ -374,7 +376,7 @@ let variables is_install opt (args,defs) =
print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n";
print "GRAMMARS?=grammar.cma\n";
print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
- print "CAMLP4OPTIONS?=\n";
+ print "CAMLP4OPTIONS?=-loc loc\n";
print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n";
end;
match is_install with
@@ -564,18 +566,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
print "gallina: $(GFILES)\n\n";
print "html: $(GLOBFILES) $(VFILES)\n";
print "\t- mkdir -p html\n";
- print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
print "\t- mkdir -p html\n";
- print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "all.ps: $(VFILES)\n";
- print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "all-gal.ps: $(VFILES)\n";
- print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "all.pdf: $(VFILES)\n";
- print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "all-gal.pdf: $(VFILES)\n";
- print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "validate: $(VOFILES)\n";
print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n";
print "beautify: $(VFILES:=.beautified)\n";