diff options
| author | Enrico Tassi | 2014-02-25 11:01:46 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-02-26 14:53:08 +0100 |
| commit | ec8540506e27ae3f27a1ecffed1a3e9f6b6cbcb4 (patch) | |
| tree | dd25444399bc0570fc470d8bb7e02129ec39a032 | |
| parent | 45d6972565c82ddd9b7aae92f2928d500a6fc228 (diff) | |
coq_makefile: new target vi2vo
| -rw-r--r-- | tools/coq_makefile.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ab4a89ffbf..37a3e8062a 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -617,6 +617,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other 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 "gallina: $(GFILES)\n\n"; print "html: $(GLOBFILES) $(VFILES)\n"; |