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

6 files changed, 34 insertions, 43 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
 
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 1954d1682..e259da7af 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -179,25 +179,15 @@ let backtrack snum pnum naborts =
 
 (** [reset_initial] resets the system and clears the command history
     stack, only pushing back the initial entry. It should be equivalent
-    to [backto Lib.first_command_label], but sligthly more efficient. *)
+    to [backto n0] where [n0] is the first label stored in the history.
+    Note that there might be other labels before [n0] in the libstack,
+    created during evaluation of .coqrc or initial Load's. *)
 
 let reset_initial () =
-  let init_label = Lib.first_command_label in
-  if Int.equal (Lib.current_command_label ()) init_label then ()
-  else begin
-    Pfedit.delete_all_proofs ();
-    Lib.reset_label init_label;
-    Stack.clear history;
-    Stack.push
-      { label = init_label;
-	nproofs = 0;
-	prfname = None;
-	prfdepth = 0;
-	ngoals = 0;
-	reachable = true;
-	cmd = VernacNop }
-      history
-  end
+  let n = Stack.length history in
+  npop (n-1);
+  Pfedit.delete_all_proofs ();
+  Lib.reset_label (top ()).label
 
 (** Reset to the last known state just before defining [id] *)
 
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
index 5f9e9f98c..d4ac7cc61 100644
--- a/toplevel/backtrack.mli
+++ b/toplevel/backtrack.mli
@@ -60,7 +60,9 @@ val backtrack : int -> int -> int -> unit
 
 (** [reset_initial] resets the system and clears the command history
     stack, only pushing back the initial entry. It should be equivalent
-    to [backto Lib.first_command_label], but sligthly more efficient. *)
+    to [backto n0] where [n0] is the first label stored in the history.
+    Note that there might be other labels before [n0] in the libstack,
+    created during evaluation of .coqrc or initial Load's. *)
 
 val reset_initial : unit -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 498c653ab..18b5e8029 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1582,7 +1582,7 @@ let vernac_reset_initial () =
     Backtrack.reset_initial ()
   else begin
     Pp.msg_warning (str "Reset command occurred in non-interactive mode.");
-    Lib.reset_label Lib.first_command_label
+    Lib.raw_reset_initial ()
   end
 
 (* For compatibility with ProofGeneral: *)