diff options
| -rw-r--r-- | library/lib.ml | 5 | ||||
| -rw-r--r-- | library/lib.mli | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
3 files changed, 8 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml index 34958ed275..9f3ec4f5d6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -36,7 +36,10 @@ and library_segment = library_entry list let lib_stk = ref ([] : (section_path * node) list) -let default_module = make_dirpath Nametab.default_root_prefix +let default_module_name = id_of_string "Top" +let default_module = make_dirpath [default_module_name] +let init_toplevel_root () = Nametab.push_library_root default_module_name + let module_name = ref None let path_prefix = ref (default_module : dir_path) diff --git a/library/lib.mli b/library/lib.mli index b22839a3da..4c802a0f80 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -56,6 +56,9 @@ val make_path : identifier -> path_kind -> section_path val cwd : unit -> dir_path val is_section_p : dir_path -> bool +(* This is to declare the interactive toplevel default module name as a root*) +val init_toplevel_root : unit -> unit + val start_module : dir_path -> unit val end_module : module_ident -> dir_path val export_module : dir_path -> library_segment diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7d293aed9a..2c57b885e2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -215,6 +215,7 @@ let start () = exit 1 end; if !batch_mode then (flush_all(); Profile.print_profile ();exit 0); + if not (!batch_mode) then Lib.init_toplevel_root (); Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); |