diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 10 | ||||
| -rw-r--r-- | tools/coqc.ml | 4 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 4 |
3 files changed, 9 insertions, 9 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c8087f7f1..159d48599 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -329,7 +329,7 @@ let clean sds sps = print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; end; if !some_vfile then - print "\trm -f $(VOFILES) $(VOFILES:.vo=.vi) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"; + print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; print "\t- rm -rf html mlihtml uninstall_me.sh\n"; List.iter @@ -389,7 +389,7 @@ 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=.vi): %.vi: %.v\n\t$(COQC) -quick $(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"; @@ -660,9 +660,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other end; if !some_vfile then begin - print "quick:\n\t$(MAKE) -f $(firstword $(MAKEFILE_LIST)) all VO=vi\n"; - print "vi2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vi2vo $(J) $(VOFILES:%.vo=%.vi)\n"; - print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vi-checking $(J) $(VOFILES:%.vo=%.vi)\n"; + print "quick: $(VOFILES:.vo=.vio)\n\n"; + print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n"; + print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n"; print "gallina: $(GFILES)\n\n"; print "html: $(GLOBFILES) $(VFILES)\n"; print "\t- mkdir -p html\n"; diff --git a/tools/coqc.ml b/tools/coqc.ml index 12de061e0..bb15a2941 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -144,8 +144,8 @@ let parse_args () = | "-R" :: s :: "-as" :: [] -> usage () | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem - | ("-schedule-vi-checking" - |"-check-vi-tasks" | "-schedule-vi2vo" as o) :: s :: rem -> + | ("-schedule-vio-checking" + |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem -> let nodash, rem = CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in extra_arg_needed := false; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 3dd6cb444..10150497d 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -427,8 +427,8 @@ let coq_dependencies () = printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename; traite_fichier_Coq !suffixe true (name ^ ".v"); printf "\n"; - printf "%s.vi: %s.v" ename ename; - traite_fichier_Coq ".vi" true (name ^ ".v"); + printf "%s.vio: %s.v" ename ename; + traite_fichier_Coq ".vio" true (name ^ ".v"); printf "\n"; flush stdout) (List.rev !vAccu) |