Merge PR #10002: Integrate ltac2

Ack-by: JasonGross
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego

1 files changed, 3 insertions, 2 deletions

diff --git a/dune b/dune
index 787c3c3674..4beba1c14f 100644
--- a/dune
+++ b/dune
@@ -18,8 +18,9 @@
  (targets .vfiles.d)
  (deps
   (source_tree theories)
-  (source_tree plugins))
- (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins -type f -name *.v`"))))
+  (source_tree plugins)
+  (source_tree user-contrib))
+ (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins user-contrib -type f -name *.v`"))))
 
 (alias
  (name vodeps)