diff --git a/src/dune_rules/coq_module.ml b/src/dune_rules/coq_module.ml
index 3843c9fc67cf..7fe823d81297 100644
--- a/src/dune_rules/coq_module.ml
+++ b/src/dune_rules/coq_module.ml
@@ -92,7 +92,7 @@ let obj_files x ~wrapper_name ~mode ~obj_dir ~obj_files_mode =
   in
   let obj_files =
     match obj_files_mode with
-    | Build -> [ x.name ^ ".vo"; "." ^ x.name ^ ".aux"; x.name ^ ".glob" ]
+    | Build -> [ x.name ^ ".vo"; x.name ^ ".glob" ]
     | Install -> [ x.name ^ ".vo" ]
   in
   List.map obj_files ~f:(fun fname ->
diff --git a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
index 4d7f98a49528..f704c496a6a9 100644
--- a/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/base-unsound.t/run.t
@@ -1,5 +1,5 @@
   $ dune build --display short --profile unsound --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc .foo.aux,foo.{glob,vo}
-          coqc .bar.aux,bar.{glob,vo}
+          coqc foo.{glob,vo}
+          coqc bar.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/base.t/run.t b/test/blackbox-tests/test-cases/coq/base.t/run.t
index 8ac016d27fea..e5bccec4b47d 100644
--- a/test/blackbox-tests/test-cases/coq/base.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/base.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc .foo.aux,foo.{glob,vo}
-          coqc .bar.aux,bar.{glob,vo}
+          coqc foo.{glob,vo}
+          coqc bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [
diff --git a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
index 6a76d25981bd..13b65eea34ec 100644
--- a/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-cycle.t/run.t
@@ -5,7 +5,7 @@ We check cycles are detected
   -> theory B in B
   -> theory A in A
   -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/.a.aux
+  -> required by _build/default/A/a.glob
   -> required by alias A/all
   -> required by alias default
   [1]
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
index 361fdc9d64d5..223e50bd5ed4 100644
--- a/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-installed.t/run.t
@@ -13,7 +13,7 @@ TODO: Currently this is not supported so the output is garbage
   Theory B not found
   -> required by theory A in .
   -> required by _build/default/a.v.d
-  -> required by _build/default/.a.aux
+  -> required by _build/default/a.glob
   -> required by alias all
   -> required by alias default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
index 78b691f29224..578cf0d9c898 100644
--- a/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-plugin.t/run.t
@@ -23,5 +23,5 @@
       ocamlopt src_b/ml_plugin_b.{a,cmxa}
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
-          coqc thy1/.a.aux,thy1/a.{glob,vo}
-          coqc thy2/.a.aux,thy2/a.{glob,vo}
+          coqc thy1/a.{glob,vo}
+          coqc thy2/a.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
index acf813e8090d..653d55ace160 100644
--- a/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-cycle.t/run.t
@@ -8,7 +8,9 @@ dependencies.
   -> theory C in C
   -> theory A in A
   -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/.a.aux
+  -> required by _build/default/A/a.vo
+  -> required by _build/install/default/lib/coq/user-contrib/A/a.vo
+  -> required by _build/default/A/A.install
   -> required by alias A/all
   -> required by alias A/default
   [1]
@@ -20,7 +22,9 @@ dependencies.
   -> theory A in A
   -> theory B in B
   -> required by _build/default/B/b.v.d
-  -> required by _build/default/B/.b.aux
+  -> required by _build/default/B/b.vo
+  -> required by _build/install/default/lib/coq/user-contrib/B/b.vo
+  -> required by _build/default/B/B.install
   -> required by alias B/all
   -> required by alias B/default
   [1]
@@ -32,7 +36,9 @@ dependencies.
   -> theory B in B
   -> theory C in C
   -> required by _build/default/C/c.v.d
-  -> required by _build/default/C/.c.aux
+  -> required by _build/default/C/c.vo
+  -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
+  -> required by _build/default/C/C.install
   -> required by alias C/all
   -> required by alias C/default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
index 61d86ca1a84f..7295c8e38cd4 100644
--- a/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-projects-missing.t/run.t
@@ -9,7 +9,9 @@ dependency.
   -> required by theory B in B
   -> required by theory C in C
   -> required by _build/default/C/c.v.d
-  -> required by _build/default/C/.c.aux
+  -> required by _build/default/C/c.vo
+  -> required by _build/install/default/lib/coq/user-contrib/C/c.vo
+  -> required by _build/default/C/C.install
   -> required by alias C/all
   -> required by alias C/default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
index 3bb751183049..94f362f5ac4a 100644
--- a/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-self.t/run.t
@@ -3,7 +3,7 @@ Composing a theory with itself should cause a cycle
   Error: Dependency cycle between:
      theory A in A
   -> required by _build/default/A/a.v.d
-  -> required by _build/default/A/.a.aux
+  -> required by _build/default/A/a.glob
   -> required by alias A/all
   -> required by alias default
   [1]
diff --git a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
index 24b83fc9991f..536144c99886 100644
--- a/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/run.t
@@ -17,9 +17,9 @@
         coqdep a/a.v.d
         coqdep b/b.v.d
         coqdep b/d.v.d
-          coqc a/.a.aux,a/a.{glob,vo}
-          coqc b/.b.aux,b/b.{glob,vo}
-          coqc b/.d.aux,b/d.{glob,vo}
+          coqc a/a.{glob,vo}
+          coqc b/b.{glob,vo}
+          coqc b/d.{glob,vo}
   $ cat > b/b.v <<EOF
   > From a Require Import a.
   > Definition bar := a.foo.
@@ -27,4 +27,4 @@
   > EOF
   $ dune build --display short --debug-dependency-path
         coqdep b/b.v.d
-          coqc b/.b.aux,b/b.{glob,vo}
+          coqc b/b.{glob,vo}
diff --git a/test/blackbox-tests/test-cases/coq/coqtop-recomp.t b/test/blackbox-tests/test-cases/coq/coqtop-recomp.t
index b9c992cffd26..4cc56d9d6694 100644
--- a/test/blackbox-tests/test-cases/coq/coqtop-recomp.t
+++ b/test/blackbox-tests/test-cases/coq/coqtop-recomp.t
@@ -21,7 +21,7 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   $ dune coq top --display short --toplevel echo dir/bar.v
         coqdep dir/bar.v.d
         coqdep dir/foo.v.d
-          coqc dir/.foo.aux,dir/foo.{glob,vo}
+          coqc dir/foo.{glob,vo}
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune coq top --display short --toplevel echo dir/bar.v
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
@@ -30,7 +30,7 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   Entering directory '..'
         coqdep dir/bar.v.d
         coqdep dir/foo.v.d
-          coqc dir/.foo.aux,dir/foo.{glob,vo}
+          coqc dir/foo.{glob,vo}
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
   $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
   Entering directory '..'
diff --git a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t
index 0f8a193571cc..b6cfeccb553a 100644
--- a/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/ml-lib.t/run.t
@@ -22,4 +22,4 @@
       ocamlopt src_b/ml_plugin_b.{a,cmxa}
       ocamlopt src_a/ml_plugin_a.cmxs
       ocamlopt src_b/ml_plugin_b.cmxs
-          coqc theories/.a.aux,theories/a.{glob,vo}
+          coqc theories/a.{glob,vo}
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
index c1c724c7045d..4981aec7e5b4 100644
--- a/test/blackbox-tests/test-cases/coq/native-compose.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/native-compose.t/run.t
@@ -2,9 +2,9 @@
         coqdep bar/bar.v.d
         coqdep foo/foo.v.d
         coqdep foo/a/a.v.d
-          coqc foo/.foo.aux,foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo}
-          coqc foo/a/.a.aux,foo/a/Nfoo_a_a.{cmi,cmxs},foo/a/a.{glob,vo}
-          coqc bar/.bar.aux,bar/Nbar_baz_bar.{cmi,cmxs},bar/bar.{glob,vo}
+          coqc foo/Nfoo_foo.{cmi,cmxs},foo/foo.{glob,vo}
+          coqc foo/a/Nfoo_a_a.{cmi,cmxs},foo/a/a.{glob,vo}
+          coqc bar/Nbar_baz_bar.{cmi,cmxs},bar/bar.{glob,vo}
 
   $ dune build --profile=release --debug-dependency-path @default
   lib: [
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
index 1b01b367361f..fa6122475979 100644
--- a/test/blackbox-tests/test-cases/coq/native-single.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/native-single.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --profile=release --display short --debug-dependency-path @all
         coqdep bar.v.d
         coqdep foo.v.d
-          coqc .foo.aux,Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
-          coqc .bar.aux,Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
+          coqc Nbasic_foo.{cmi,cmxs},foo.{glob,vo}
+          coqc Nbasic_bar.{cmi,cmxs},bar.{glob,vo}
 
   $ dune build --profile=release --debug-dependency-path @default
   lib: [
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
index 99fba5a0cc98..f928963911d5 100644
--- a/test/blackbox-tests/test-cases/coq/rec-module.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/rec-module.t/run.t
@@ -3,10 +3,10 @@
         coqdep b/foo.v.d
         coqdep c/d/bar.v.d
         coqdep c/ooo.v.d
-          coqc b/.foo.aux,b/foo.{glob,vo}
-          coqc c/d/.bar.aux,c/d/bar.{glob,vo}
-          coqc c/.ooo.aux,c/ooo.{glob,vo}
-          coqc a/.bar.aux,a/bar.{glob,vo}
+          coqc b/foo.{glob,vo}
+          coqc c/d/bar.{glob,vo}
+          coqc c/ooo.{glob,vo}
+          coqc a/bar.{glob,vo}
 
   $ dune build --debug-dependency-path @default
   lib: [