Re-allow Reset in compiled files

 This was a wish by A. Chlipala on coq-club

 Both Reset foo and Reset Initial are accepted (with a warning).
 If some proofs were opened, all of them are aborted. This isn't the
 behavior of the interactive Reset that has more information and can
 be more selective, but this shouldn't be a big issue in practice.

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

1 files changed, 21 insertions, 4 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d4cacf68b..7843d10b4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1445,10 +1445,27 @@ let vernac_back n =
   with Backtrack.Invalid -> error "Invalid backtrack."
 
 let vernac_reset_name id =
-  try Backtrack.reset_name id; try_print_subgoals ()
-  with Backtrack.Invalid -> error "Invalid Reset."
-
-let vernac_reset_initial () = Backtrack.reset_initial ()
+  try
+    if Backtrack.is_active () then
+      (Backtrack.reset_name id; try_print_subgoals ())
+    else
+      (* When compiling files, Reset is now allowed again
+	 as asked by A. Chlipala. we emulate a simple reset,
+	 that discards all proofs. *)
+      let lbl = Lib.label_before_name id in
+      Pfedit.delete_all_proofs ();
+      Pp.msg_warning (str "Reset occured during compilation.");
+      Lib.reset_label lbl
+  with Backtrack.Invalid | Not_found -> error "Invalid Reset."
+
+
+let vernac_reset_initial () =
+  if Backtrack.is_active () then
+    Backtrack.reset_initial ()
+  else begin
+    Pp.msg_warning (str "Reset occured during compilation.");
+    Lib.reset_label Lib.first_command_label
+  end
 
 (* For compatibility with ProofGeneral: *)