Also allow Reset in Load'ed files

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

2 files changed, 3 insertions, 3 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6bc544aaad..9fd471708e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -348,6 +348,7 @@ let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
+    Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
     read_vernac_file verb file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with e ->
@@ -360,7 +361,6 @@ let compile verbosely f =
   Dumpglob.start_dump_glob long_f_dot_v;
   Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
   if !Flags.xml_export then !xml_start_library ();
-  Lib.mark_end_of_command ();
   let _ = load_vernac verbosely long_f_dot_v in
   if Pfedit.get_all_proof_names () <> [] then
     (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7843d10b44..e100025dd8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1454,7 +1454,7 @@ let vernac_reset_name id =
 	 that discards all proofs. *)
       let lbl = Lib.label_before_name id in
       Pfedit.delete_all_proofs ();
-      Pp.msg_warning (str "Reset occured during compilation.");
+      Pp.msg_warning (str "Reset command occurred in non-interactive mode.");
       Lib.reset_label lbl
   with Backtrack.Invalid | Not_found -> error "Invalid Reset."
 
@@ -1463,7 +1463,7 @@ let vernac_reset_initial () =
   if Backtrack.is_active () then
     Backtrack.reset_initial ()
   else begin
-    Pp.msg_warning (str "Reset occured during compilation.");
+    Pp.msg_warning (str "Reset command occurred in non-interactive mode.");
     Lib.reset_label Lib.first_command_label
   end