aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tools/coq_dune.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index ab180769b6..f62947ec67 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -170,6 +170,7 @@ let pp_rule fmt targets deps action =
let gen_coqc_targets vo =
[ vo.target
; replace_ext ~file:vo.target ~newext:".glob"
+ ; replace_ext ~file:vo.target ~newext:".vos"
; "." ^ replace_ext ~file:vo.target ~newext:".aux"]
(* Generate the dune rule: *)