Merge PR #11075: load .vo when .vos is missing + misc vos changes

Reviewed-by: gares
Reviewed-by: silene

9 files changed, 0 insertions, 12 deletions

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