From ec8540506e27ae3f27a1ecffed1a3e9f6b6cbcb4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 25 Feb 2014 11:01:46 +0100
Subject: coq_makefile: new target vi2vo

---
 tools/coq_makefile.ml | 1 +
 1 file changed, 1 insertion(+)

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";
-- 
cgit v1.2.3