bug #909: Top n'est cree que si le contexte est vide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7602 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 13 insertions, 5 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 737f771841..9b638427cb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -426,11 +426,13 @@ type compiled_library =
 (* We check that only initial state Require's were performed before 
    [start_library] was called *)
 
+let is_empty senv =
+  senv.revsign = [] &&
+  senv.modinfo.msid = initial_msid &&
+  senv.modinfo.variant = NONE
+
 let start_library dir senv =
-  if not (senv.revsign = [] &&
-	  senv.modinfo.msid = initial_msid &&
-	  senv.modinfo.variant = NONE)
-  then
+  if not (is_empty senv) then
     anomaly "Safe_typing.start_library: environment should be empty";
   let dir_path,l = 
     match (repr_dirpath dir) with
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 9b5d78870f..83aa3e9433 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -28,6 +28,7 @@ type safe_environment
 val env_of_safe_env : safe_environment -> Environ.env
 
 val empty_environment : safe_environment
+val is_empty : safe_environment -> bool
 
 (* Adding and removing local declarations (Local or Variables) *)
 val push_named_assum :
diff --git a/library/global.ml b/library/global.ml
index 6606200866..b8bc364b05 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -25,6 +25,8 @@ let safe_env () = !global_env
 
 let env () = env_of_safe_env !global_env
 
+let env_is_empty () = is_empty !global_env
+
 let _ = 
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
diff --git a/library/global.mli b/library/global.mli
index 9468f3ef52..ef8472d08f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -29,6 +29,8 @@ open Safe_typing
 val safe_env : unit -> safe_environment
 val env : unit -> Environ.env
 
+val env_is_empty : unit -> bool
+
 val universes : unit -> universes
 val named_context : unit -> Sign.named_context
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 56f6b111e2..7633e168f9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -316,7 +316,8 @@ let init is_ide =
       inputstate ();
       set_vm_opt ();
       engage ();
-      if not !batch_mode then Declaremods.start_library !toplevel_name;
+      if not !batch_mode && Global.env_is_empty() then
+        Declaremods.start_library !toplevel_name;
       init_library_roots ();
       load_vernac_obj ();
       require ();