aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b948a0535..1854e1126 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -857,7 +857,7 @@ let vernac_add_loadpath isrec pdir ldiropt =
let pdir = expand pdir in
let alias = Option.default Nameops.default_root_prefix ldiropt in
(if isrec then Mltop.add_rec_path else Mltop.add_path)
- ~unix_path:pdir ~coq_root:alias
+ ~unix_path:pdir ~coq_root:alias ~implicit:true
let vernac_remove_loadpath path =
Loadpath.remove_load_path (expand path)