aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 933b23c53..7546ad310 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -321,7 +321,7 @@ let init is_ide =
set_vm_opt ();
engage ();
if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
- option_iter Declaremods.start_library !toplevel_name;
+ Option.iter Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();