diff --git a/CHANGES.md b/CHANGES.md
index 70242c6fa8c4..de8347c98760 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,8 @@
+Unreleased
+----------
+
+- Add missing `.aux` targets to coq rules (3721, fixes #3437, @rgrinberg)
+
 2.7.0 (13/08/2020)
 ------------------
 
diff --git a/src/dune/coq_module.ml b/src/dune/coq_module.ml
index edb10c53d79b..e888f768e250 100644
--- a/src/dune/coq_module.ml
+++ b/src/dune/coq_module.ml
@@ -41,6 +41,10 @@ let dep_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".v.d")
 
+let aux_file x ~obj_dir =
+  let vo_dir = build_vo_dir ~obj_dir x in
+  Path.Build.relative vo_dir ("." ^ x.name ^ ".aux")
+
 let obj_file x ~obj_dir =
   let vo_dir = build_vo_dir ~obj_dir x in
   Path.Build.relative vo_dir (x.name ^ ".vo")
diff --git a/src/dune/coq_module.mli b/src/dune/coq_module.mli
index 9cc3ad8caef4..2b82f963d051 100644
--- a/src/dune/coq_module.mli
+++ b/src/dune/coq_module.mli
@@ -38,6 +38,8 @@ val name : t -> Name.t
 
 val dep_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
+val aux_file : t -> obj_dir:Path.Build.t -> Path.Build.t
+
 val obj_file : t -> obj_dir:Path.Build.t -> Path.Build.t
 
 val to_dyn : t -> Dyn.t
diff --git a/src/dune/coq_rules.ml b/src/dune/coq_rules.ml
index b420cdf01fe8..57a85630bac8 100644
--- a/src/dune/coq_rules.ml
+++ b/src/dune/coq_rules.ml
@@ -265,7 +265,8 @@ let coqc_rule (cctx : _ Context.t) ~file_flags coq_module =
   let source = Coq_module.source coq_module in
   let file_flags =
     let object_to = Coq_module.obj_file ~obj_dir:cctx.dir coq_module in
-    [ Command.Args.Hidden_targets [ object_to ]
+    let aux = Coq_module.aux_file ~obj_dir:cctx.dir coq_module in
+    [ Command.Args.Hidden_targets [ object_to; aux ]
     ; S file_flags
     ; Command.Args.Dep (Path.build source)
     ]
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 1f3dff28324b..c6f7a11885d6 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.vo
-          coqc bar.vo
+          coqc .foo.aux,foo.vo
+          coqc .bar.aux,bar.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 82f66a4f873c..626cbbcfc467 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.vo
-          coqc bar.vo
+          coqc .foo.aux,foo.vo
+          coqc .bar.aux,bar.vo
 
   $ dune build --debug-dependency-path @default
   lib: [
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 e9f10fc1a8b3..8f7ff81fa937 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.vo
-          coqc thy2/a.vo
+          coqc thy1/.a.aux,thy1/a.vo
+          coqc thy2/.a.aux,thy2/a.vo
diff --git a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
index 9c89607a296d..32e0f50a88b0 100644
--- a/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-simple.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path
         coqdep a/a.v.d
         coqdep b/b.v.d
-          coqc a/a.vo
-          coqc b/b.vo
+          coqc a/.a.aux,a/a.vo
+          coqc b/.b.aux,b/b.vo
   lib: [
     "_build/install/default/lib/csimple/META"
     "_build/install/default/lib/csimple/dune-package"
diff --git a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
index c615b3c7c833..85213f5f811c 100644
--- a/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
+++ b/test/blackbox-tests/test-cases/coq/compose-sub-theory.t/run.t
@@ -1,8 +1,8 @@
   $ dune build --display short --debug-dependency-path
         coqdep b/b.v.d
         coqdep a/a.v.d
-          coqc a/a.vo
-          coqc b/b.vo
+          coqc a/.a.aux,a/a.vo
+          coqc b/.b.aux,b/b.vo
   lib: [
     "_build/install/default/lib/subtheory/META"
     "_build/install/default/lib/subtheory/dune-package"
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 58fea14f94d7..5e7b3099ce49 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.vo
+          coqc theories/.a.aux,theories/a.vo
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 de001841ab52..6690b3fa74c6 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.vo
-          coqc c/d/bar.vo
-          coqc c/ooo.vo
-          coqc a/bar.vo
+          coqc b/.foo.aux,b/foo.vo
+          coqc c/d/.bar.aux,c/d/bar.vo
+          coqc c/.ooo.aux,c/ooo.vo
+          coqc a/.bar.aux,a/bar.vo
 
   $ dune build --debug-dependency-path @default
   lib: [