Fix issues with "Reset Initial" in scripts given to coqtop -l

 Doing coqtop -l on a file starting with Reset Initial used to fail.
 To avoid that, we now always place an initial DOT in the libstack.

 Backtrack.reset_initial has been adapted accordingly: during an
 interactive session following a Load via coqtop -l (or .coqrc),
 a Reset Initial will bring back at the start of the interactive
 session, *not* undoing the initial Load.

 Note : Reset Initial might hence not be equivalent anymore to BackTo 1.

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

3 files changed, 23 insertions, 24 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index cf333a886..5866d612e 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -223,10 +223,10 @@ let conv_names_do_module exists what iter_objects i ((sp,kn),substobjs) =
   let dir = dir_of_sp sp and mp = mp_of_kn kn in
   do_module exists what iter_objects i dir mp substobjs []
 
-(* Interactive modules and module types cannot be recached! cache_mod*
-   functions can be called only once (and "end_mod*" set the flag to
-   false then)
-*)
+(* Nota: Interactive modules and module types cannot be recached!
+   This used to be checked here via a flag along the substobjs.
+   The check is still there for module types (see cache_modtype). *)
+
 let cache_module ((sp,kn),substobjs) =
   let dir = dir_of_sp sp and mp = mp_of_kn kn in
   do_module false "cache" load_objects 1 dir mp substobjs []
diff --git a/library/lib.ml b/library/lib.ml
index c7454edaf..e33bf5b15 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -282,7 +282,6 @@ let start_mod is_type export id mp fs =
   add_entry oname (OpenedModule (is_type,export,prefix,fs));
   path_prefix := prefix;
   prefix
-(*  add_frozen_state () must be called in declaremods *)
 
 let start_module = start_mod false
 let start_modtype = start_mod true None
@@ -307,8 +306,6 @@ let end_mod is_type =
   add_entry oname (ClosedModule (List.rev (mark::after)));
   let prefix = !path_prefix in
   recalc_path_prefix ();
-  (* add_frozen_state must be called after processing the module,
-     because we cannot recache interactive modules  *)
   (oname, prefix, fs, after)
 
 let end_module () = end_mod false
@@ -407,7 +404,8 @@ let sectab =
     ~name:"section-context"
 
 let add_section () =
-  sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
+  sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
+                (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
 let add_section_variable id impl =
   match !sectab with
@@ -550,15 +548,13 @@ let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
-  let spf = match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) -> Summary.unfreeze_summaries f; sp
+  (* Always at least one frozen state in the libstack *)
+  match find_entry_p is_frozen_state with
+    | (sp, FrozenState f) ->
+      Summary.unfreeze_summaries f;
+      let (after,_,_) = split_lib sp in
+      recache_context after
     | _ -> assert false
-  in
-  let (after,_,_) = split_lib spf in
-  try
-    recache_context after
-  with
-    | Not_found -> error "Tried to set environment to an incoherent state."
 
 let reset_to test =
   let (_,_,before) = split_lib_gen test in
@@ -591,6 +587,8 @@ let reset_label n =
   (* forget state numbers after n only if reset succeeded *)
   reset_command_label n
 
+let raw_reset_initial () = reset_label first_command_label
+
 (** Search the last label registered before defining [id] *)
 
 let label_before_name (loc,id) =
@@ -618,11 +616,10 @@ let unfreeze (mn,stk) =
   recalc_path_prefix ()
 
 let init () =
-  lib_stk := [];
-  add_frozen_state ();
-  comp_name := None;
-  path_prefix := initial_prefix;
-  Summary.init_summaries ()
+  unfreeze (None,[]);
+  Summary.init_summaries ();
+  add_frozen_state (); (* Stores e.g. the keywords declared in g_*.ml4 *)
+  mark_end_of_command () (* For allowing Reset Initial in coqtop -l *)
 
 (* Misc *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 1ea76f1ad..a37d7a113 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -155,14 +155,16 @@ val mark_end_of_command : unit -> unit
 (** Returns the current label number *)
 val current_command_label : unit -> int
 
-(** The first label number *)
-val first_command_label : int
-
 (** [reset_label n] resets [lib_stk] to the label n registered by
    [mark_end_of_command()]. It forgets anything registered after
    this label. The label should be strictly in the past. *)
 val reset_label : int -> unit
 
+(** [raw_reset_initial] is now [reset_label] to the first label.
+    This is meant to be used during initial Load's and compilations.
+    Otherwise, consider instead [Backtrack.reset_initial] *)
+val raw_reset_initial : unit -> unit
+
 (** search the label registered immediately before adding some definition *)
 val label_before_name : Names.Id.t Loc.located -> int