5 files changed, 58 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/quick2vo/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh
new file mode 100755
index 000000000..9e681223b
--- /dev/null
+++ b/test-suite/coq-makefile/quick2vo/run.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+a=`uname`
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+# vio2vo is broken on Windows (#6720)
+if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then
+    make quick2vo J=2
+    test -f theories/test.vo
+    make validate
+fi
diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/vio2vo/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh
new file mode 100755
index 000000000..85656da41
--- /dev/null
+++ b/test-suite/coq-makefile/vio2vo/run.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+a=`uname`
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make quick
+# vio2vo is broken on Windows (#6720)
+if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then
+    make vio2vo J=2
+    test -f theories/test.vo
+    make validate
+fi
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 173eaae89..23212ef84 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -382,7 +382,7 @@ bytefiles: $(CMOFILES) $(CMAFILES)
 optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
-# FIXME, see Ralph's bugreport
+# FIXME, see Ralf's bugreport
 quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
 
@@ -391,6 +391,18 @@ vio2vo:
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
+quick2vo:
+	$(HIDE)make -j $(J) quick
+	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
+	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
+	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
+	done); \
+	echo "VIO2VO: $$VIOFILES"; \
+	if [ -n "$$VIOFILES" ]; then \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
+	fi
+.PHONY: quick2vo
+
 checkproofs:
 	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)