Safe_typing code refactoring

 - No more modinfo sub-record in the safe_environment record,
   this was a syntactic pain.
     senv.modinfo.modpath --> senv.modpath
     senv.modinfo.variant --> senv.modvariant
     senv.modinfo.resolver --> senv.modresolver
     senv.modinfo.resolver_of_param --> senv.paramresolver
     senv.modinfo.label : removed (can be inferred from modpath)

 - No more systematic chaining of safe_environment ('old' field).
   Instead, earlier safe_environment is stored in the modvariant field
   when necessary (STRUCT and SIG case).

 - Improved sharing between end_module and end_modtype

 - More qualified names instead of open, better comments, ...

 - Some user errors are now checked earlier elsewhere (see for
   instance vernac_end_segment), so we can turn these errors into
   asserts. The user error about higher-order include is now algebraic.

 - Highlight the idea of a state monad in Safe_typing :
   type 'a safe_transformer = safe_environment -> 'a * safe_environment
   More systematic code in Global, thanks to 'globalize' function.

 - Declaremods : less informations stored in openmod_info

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

1 files changed, 3 insertions, 2 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 26e3081bb..c0b47f0c1 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -395,8 +395,9 @@ let init arglist =
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
       Syntax_def.set_compat_notations (not !no_compat_ntn);
-      if (not !batch_mode|| List.is_empty !compile_list) && Global.env_is_empty() then
-        Option.iter Declaremods.start_library !toplevel_name;
+      if (not !batch_mode || List.is_empty !compile_list)
+         && Global.env_is_initial ()
+      then Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
       load_vernac_obj ();
       require ();