aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_boot.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_boot.ml')
-rw-r--r--tools/coqdep_boot.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 588bf2dcf..f42c8dc75 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -38,6 +38,7 @@ let coqdep_boot () =
else begin
add_rec_dir add_known "theories" ["Coq"];
add_rec_dir add_known "plugins" ["Coq"];
+ add_dir add_known "tactics" [];
end;
if !option_c then mL_dependencies ();
coq_dependencies ()