Merge PR #8642: Compiled interfaces with -vos and -vok options

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

9 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 88237815b1..0d9b9ea867 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -28,10 +28,12 @@ sort -u > desired <<EOT
 ./test/test.glob
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 ./test/sub
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
+./test/sub/testsub.vos
 ./test/mlihtml
 ./test/mlihtml/index_exceptions.html
 ./test/mlihtml/index.html
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 5811dd17e4..852ac372f4 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -26,10 +26,12 @@ sort -u > desired <<EOT
 ./test/test.glob
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 ./test/sub
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
+./test/sub/testsub.vos
 ./test/mlihtml
 ./test/mlihtml/index_exceptions.html
 ./test/mlihtml/index.html
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index bbd2fc460c..1303aa90b6 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -19,5 +19,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index bbd2fc460c..1303aa90b6 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -19,5 +19,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 45bf1481df..3a5425c8bf 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -29,10 +29,12 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 ./test2
 ./test2/test.glob
 ./test2/test.v
 ./test2/test.vo
+./test2/test.vos
 ./orphan_test_test2_test
 ./orphan_test_test2_test/html
 ./orphan_test_test2_test/html/coqdoc.css
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 8f9ab9a711..588de82613 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -22,6 +22,7 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 ./test/.coq-native
 ./test/.coq-native/Ntest_test.cmi
 ./test/.coq-native/Ntest_test.cmx
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index 1e2bd979b3..cd47187582 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -22,5 +22,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index 1e2bd979b3..cd47187582 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -22,5 +22,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index 1e2bd979b3..cd47187582 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -22,5 +22,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
+./test/test.vos
 EOT
 exec diff -u desired actual