From 37293bd104434bb15acc7d46b8cba90e70504aac Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 5 Jul 2016 15:58:20 +0200 Subject: Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896). Coqc now expects physical names for input files, so fix coq_makefile accordingly. --- tools/coq_makefile.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tools/coq_makefile.ml') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 381e8d08c..617185b8f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -414,9 +414,9 @@ let implicit () = print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; in let v_rules () = - print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; + print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; + print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n"; print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; @@ -424,7 +424,7 @@ in print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" + print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n" in if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); -- cgit v1.2.3