aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/mltop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/mltop.ml')
-rw-r--r--toplevel/mltop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 0a5b92270..b6690fe47 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -411,7 +411,7 @@ let inMLModule : ml_module_object -> obj =
let declare_ml_modules local l =
let l = List.map mod_of_name l in
- Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l})
+ Lib.add_anonymous_leaf ~cache_first:false (inMLModule {mlocal=local; mnames=l})
let print_ml_path () =
let l = !coq_mlpath_copy in