From a03ac1f334ed9d6cc28a199573f372219e0aad87 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Sep 2001 13:12:53 +0000
Subject: Bug default module name (2eme)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1924 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml     | 5 ++++-
 library/lib.mli    | 3 +++
 toplevel/coqtop.ml | 1 +
 3 files changed, 8 insertions(+), 1 deletion(-)

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();
-- 
cgit v1.2.3