[coq] more test for vos mode.

We check that one can go back to normal mode (without cleaning) after
having used the vos mode.

Signed-off-by: Rodolphe Lepigre <rodolphe@bedrocksystems.com>

test/blackbox-tests/test-cases/coq/vos-build.t/dune-vo

@@ -0,0 +1,9 @@
+(coq.theory
+ (name basic)
+ (package base)
+ (modules :standard)
+ (synopsis "Test Coq library"))
+
+(rule
+ (alias default)
+ (action (echo "%{read:base.install}")))

test/blackbox-tests/test-cases/coq/vos-build.t/run.t

@@ -30,3 +30,22 @@
     "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"}
     "_build/install/default/lib/coq/user-contrib/basic/foo.vos" {"coq/user-contrib/basic/foo.vos"}
   ]
+
+Checking that we can go back to vo mode (without cleaning).
+
+  $ mv dune-vo dune
+  $ dune build --display short --debug-dependency-path @all
+          coqc foo.{glob,vo}
+          coqc bar.{glob,vo}
+  $ dune build --debug-dependency-path @default
+  lib: [
+    "_build/install/default/lib/base/META"
+    "_build/install/default/lib/base/dune-package"
+    "_build/install/default/lib/base/opam"
+  ]
+  lib_root: [
+    "_build/install/default/lib/coq/user-contrib/basic/bar.v" {"coq/user-contrib/basic/bar.v"}
+    "_build/install/default/lib/coq/user-contrib/basic/bar.vo" {"coq/user-contrib/basic/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/basic/foo.v" {"coq/user-contrib/basic/foo.v"}
+    "_build/install/default/lib/coq/user-contrib/basic/foo.vo" {"coq/user-contrib/basic/foo.vo"}
+  ]