ocaml · ejgallego · May 31, 2024 · May 30, 2024
diff --git a/doc/changes/10602.md b/doc/changes/10602.md
@@ -0,0 +1 @@
+- install `.glob` files for Coq theories too (#10602, @ejgallego)
diff --git a/src/dune_rules/coq/coq_module.ml b/src/dune_rules/coq/coq_module.ml
@@ -76,6 +76,17 @@ let glob_file x ~obj_dir =
   Path.Build.relative vo_dir (x.name ^ ".glob")
 ;;
 
+(* As of today we do the same for build and install, it used not to be
+   the case *)
+let standard_obj_files ~(mode : Coq_mode.t) _obj_files_mode name =
+  let ext, glob =
+    match mode with
+    | VosOnly -> ".vos", []
+    | _ -> ".vo", [ name ^ ".glob" ]
+  in
+  [ name ^ ext ] @ glob
+;;
+
 (* XXX: Remove the install .coq-native hack once rules can output targets in
    multiple subdirs *)
 let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
@@ -92,13 +103,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
         cmxs_obj
     | VoOnly | VosOnly | Legacy -> []
   in
-  let obj_files =
-    match obj_files_mode with
-    | Build when mode = VosOnly -> [ x.name ^ ".vos" ]
-    | Build -> [ x.name ^ ".vo"; x.name ^ ".glob" ]
-    | Install when mode = VosOnly -> [ x.name ^ ".vos" ]
-    | Install -> [ x.name ^ ".vo" ]
-  in
+  let obj_files = standard_obj_files ~mode obj_files_mode x.name in
   List.map obj_files ~f:(fun fname ->
     Path.Build.relative vo_dir fname, Filename.concat install_vo_dir fname)
   @ native_objs

diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t
@@ -18,8 +18,10 @@
     "_build/install/default/lib/base/opam"
   ]
   lib_root: [
+    "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"}
     "_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.glob" {"coq/user-contrib/basic/foo.glob"}
     "_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"}
   ]
diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-compat.t/run.t
@@ -40,6 +40,7 @@ so this also tests that it won't be a problem.
   Installing $TESTCASE_ROOT/lib/B/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
 

diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-rebuild.t/run.t
@@ -33,6 +33,7 @@ so this also tests that it won't be a problem.
   Installing $TESTCASE_ROOT/lib/B/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
 
@@ -62,6 +63,8 @@ Next we update B and install it again.
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
@@ -101,10 +104,13 @@ Next we add a new file to B that should cause a call to coqdep, but no rebuild.
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_c.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_c.cmxs
+  Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.vo
 

diff --git a/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t
@@ -42,10 +42,12 @@ so this also tests that it won't be a problem.
   Installing $TESTCASE_ROOT/lib/global/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.vo
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.vo
 
@@ -76,10 +78,12 @@ somewhere else.
   Deleting $TESTCASE_ROOT/lib/global/dune-package
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs
+  Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.glob
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.v
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.vo
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs
+  Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.glob
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.v
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.vo
   Deleting empty directory $TESTCASE_ROOT/lib/global
@@ -93,10 +97,12 @@ somewhere else.
   Installing $TESTCASE_ROOT/another-place/lib/global/dune-package
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs
+  Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/b_alg.glob
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/b_alg.v
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/algebra/b_alg.vo
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs
+  Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/b_field.glob
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/b_field.v
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global/field/b_field.vo
   $ rmdir lib/coq/user-contrib/global
@@ -195,10 +201,12 @@ with the loadpath semantics of Coq.
   Installing $TESTCASE_ROOT/lib/global/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/.coq-native/Nglobal_algebra_b_alg.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/algebra/b_alg.vo
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/.coq-native/Nglobal_field_b_field.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/global/field/b_field.vo
 

diff --git a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t
@@ -34,6 +34,7 @@ so this also tests that it won't be a problem.
   Installing $TESTCASE_ROOT/lib/B/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
 
@@ -52,6 +53,7 @@ somewhere else.
   Deleting $TESTCASE_ROOT/lib/B/dune-package
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Deleting $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
   Deleting empty directory $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native
@@ -63,6 +65,7 @@ somewhere else.
   Installing $TESTCASE_ROOT/another-place/lib/B/dune-package
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/b.glob
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/another-place/lib/coq/user-contrib/B/b.vo
 
@@ -111,6 +114,7 @@ with the loadpath semantics of Coq.
   Installing $TESTCASE_ROOT/lib/B/dune-package
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmi
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/.coq-native/NB_b.cmxs
+  Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.glob
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.v
   Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/b.vo
 

diff --git a/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t b/test/blackbox-tests/test-cases/coq/compose-two-scopes.t/run.t
@@ -10,6 +10,7 @@
     "_build/install/default/lib/cvendor/opam"
   ]
   lib_root: [
+    "_build/install/default/lib/coq/user-contrib/b/b.glob" {"coq/user-contrib/b/b.glob"}
     "_build/install/default/lib/coq/user-contrib/b/b.v" {"coq/user-contrib/b/b.v"}
     "_build/install/default/lib/coq/user-contrib/b/b.vo" {"coq/user-contrib/b/b.vo"}
   ]
diff --git a/test/blackbox-tests/test-cases/coq/config-no-coqc.t/run.t b/test/blackbox-tests/test-cases/coq/config-no-coqc.t/run.t
@@ -51,6 +51,7 @@ We first test the package builds as normal, when both are in scope:
     "_build/install/default/lib/example-coq/opam"
   ]
   lib_root: [
+    "_build/install/default/lib/coq/user-contrib/Common/Foo.glob" {"coq/user-contrib/Common/Foo.glob"}
     "_build/install/default/lib/coq/user-contrib/Common/Foo.v" {"coq/user-contrib/Common/Foo.v"}
     "_build/install/default/lib/coq/user-contrib/Common/Foo.vo" {"coq/user-contrib/Common/Foo.vo"}
   ]
@@ -112,9 +113,8 @@ Coq package should fail:
 
   $ (unset INSIDE_DUNE; PATH=_path dune build -p example-coq)
   Couldn't find Coq standard library, and theory is not using (stdlib no)
-  -> required by _build/default/coq/extracted/CRelationClasses.ml
-  -> required by _build/default/coq/CRelationClasses.ml
-  -> required by _build/install/default/lib/example-coq/coq/CRelationClasses.ml
+  -> required by _build/default/coq/Common/Foo.glob
+  -> required by _build/install/default/lib/coq/user-contrib/Common/Foo.glob
   -> required by _build/default/example-coq.install
   -> required by alias install
   [1]

diff --git a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t
@@ -22,14 +22,17 @@
   lib_root: [
     "_build/install/default/lib/coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmi" {"coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmi"}
     "_build/install/default/lib/coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmxs" {"coq/user-contrib/bar/baz/.coq-native/Nbar_baz_bar.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/bar/baz/bar.glob" {"coq/user-contrib/bar/baz/bar.glob"}
     "_build/install/default/lib/coq/user-contrib/bar/baz/bar.v" {"coq/user-contrib/bar/baz/bar.v"}
     "_build/install/default/lib/coq/user-contrib/bar/baz/bar.vo" {"coq/user-contrib/bar/baz/bar.vo"}
     "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmi"}
     "_build/install/default/lib/coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs" {"coq/user-contrib/foo/.coq-native/Nfoo_foo.cmxs"}
     "_build/install/default/lib/coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmi" {"coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmi"}
     "_build/install/default/lib/coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmxs" {"coq/user-contrib/foo/a/.coq-native/Nfoo_a_a.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/foo/a/a.glob" {"coq/user-contrib/foo/a/a.glob"}
     "_build/install/default/lib/coq/user-contrib/foo/a/a.v" {"coq/user-contrib/foo/a/a.v"}
     "_build/install/default/lib/coq/user-contrib/foo/a/a.vo" {"coq/user-contrib/foo/a/a.vo"}
+    "_build/install/default/lib/coq/user-contrib/foo/foo.glob" {"coq/user-contrib/foo/foo.glob"}
     "_build/install/default/lib/coq/user-contrib/foo/foo.v" {"coq/user-contrib/foo/foo.v"}
     "_build/install/default/lib/coq/user-contrib/foo/foo.vo" {"coq/user-contrib/foo/foo.vo"}
   ]
diff --git a/test/blackbox-tests/test-cases/coq/native-single.t/run.t b/test/blackbox-tests/test-cases/coq/native-single.t/run.t
@@ -22,8 +22,10 @@
     "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"}
     "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"}
     "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"}
     "_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.glob" {"coq/user-contrib/basic/foo.glob"}
     "_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"}
   ]
diff --git a/test/blackbox-tests/test-cases/coq/per_file_flags.t/run.t b/test/blackbox-tests/test-cases/coq/per_file_flags.t/run.t
@@ -18,8 +18,10 @@
     "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_bar.cmxs"}
     "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmi"}
     "_build/install/default/lib/coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs" {"coq/user-contrib/basic/.coq-native/Nbasic_foo.cmxs"}
+    "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"}
     "_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.glob" {"coq/user-contrib/basic/foo.glob"}
     "_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"}
   ]
diff --git a/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t b/test/blackbox-tests/test-cases/coq/public-dep-on-private.t/run.t
@@ -9,9 +9,8 @@
   Theory "private" is private, it cannot be a dependency of a public theory.
   You need to associate "private" to a package.
   -> required by theory public in public/dune:2
-  -> required by _build/default/public/.public.theory.d
-  -> required by _build/default/public/b.vo
-  -> required by _build/install/default/lib/coq/user-contrib/public/b.vo
+  -> required by _build/default/public/b.glob
+  -> required by _build/install/default/lib/coq/user-contrib/public/b.glob
   -> required by _build/default/public.install
   -> required by %{read:public.install} at dune:3
   -> required by alias default in dune:1

diff --git a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t
@@ -20,12 +20,16 @@
     "_build/install/default/lib/rec/opam"
   ]
   lib_root: [
+    "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.glob" {"coq/user-contrib/rec_module/a/bar.glob"}
     "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.v" {"coq/user-contrib/rec_module/a/bar.v"}
     "_build/install/default/lib/coq/user-contrib/rec_module/a/bar.vo" {"coq/user-contrib/rec_module/a/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.glob" {"coq/user-contrib/rec_module/b/foo.glob"}
     "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.v" {"coq/user-contrib/rec_module/b/foo.v"}
     "_build/install/default/lib/coq/user-contrib/rec_module/b/foo.vo" {"coq/user-contrib/rec_module/b/foo.vo"}
+    "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.glob" {"coq/user-contrib/rec_module/c/d/bar.glob"}
     "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.v" {"coq/user-contrib/rec_module/c/d/bar.v"}
     "_build/install/default/lib/coq/user-contrib/rec_module/c/d/bar.vo" {"coq/user-contrib/rec_module/c/d/bar.vo"}
+    "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.glob" {"coq/user-contrib/rec_module/c/ooo.glob"}
     "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.v" {"coq/user-contrib/rec_module/c/ooo.v"}
     "_build/install/default/lib/coq/user-contrib/rec_module/c/ooo.vo" {"coq/user-contrib/rec_module/c/ooo.vo"}
   ]
diff --git a/test/blackbox-tests/test-cases/coq/vos-build.t/run.t b/test/blackbox-tests/test-cases/coq/vos-build.t/run.t
@@ -44,8 +44,10 @@ Checking that we can go back to vo mode (without cleaning).
     "_build/install/default/lib/base/opam"
   ]
   lib_root: [
+    "_build/install/default/lib/coq/user-contrib/basic/bar.glob" {"coq/user-contrib/basic/bar.glob"}
     "_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.glob" {"coq/user-contrib/basic/foo.glob"}
     "_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"}
   ]
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		- install `.glob` files for Coq theories too (#10602, @ejgallego)