Adds a tactic give_up.

Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals.

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

1 files changed, 12 insertions, 5 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index d91829420..496f9b87e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -540,21 +540,28 @@ let pr_open_subgoals () =
      straightforward, but seriously, [Proof.proof] should return
      [evar_info]-s instead. *)
   let p = Proof_global.give_me_the_proof () in
-  let (goals , stack , shelf, sigma ) = Proof.proof p in
+  let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in
   let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
   let seeds = Proof.V82.top_evars p in
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
-          begin match bgoals,shelf with
-	  | [],[] -> pr_subgoals None sigma seeds shelf stack goals
-          | [] , _ ->
+          begin match bgoals,shelf,given_up with
+	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
+          | [] , [] , _ ->
+	    (* emacs mode: xml-like flag for detecting information message *)
+	    str (emacs_str "<infomsg>") ++
+	    str "No more, however there are goals you gave up. You need to go back and solve them."
+	    ++ str (emacs_str "</infomsg>")
+	    ++ fnl () ++ fnl ()
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+          | [] , _ , _ ->
 	    (* emacs mode: xml-like flag for detecting information message *)
 	    str (emacs_str "<infomsg>") ++
 	    str "All the remaining goals are on the shelf."
 	    ++ str (emacs_str "</infomsg>")
 	    ++ fnl () ++ fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
-	  | _ , _ ->
+	  | _ , _, _ ->
 	    (* emacs mode: xml-like flag for detecting information message *)
 	    str (emacs_str "<infomsg>") ++
 	    str "This subproof is complete, but there are still unfocused goals."