From fb1c2f25fb0ca5f422c69e14b6b434ad1d8f01a9 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:40:19 +0000 Subject: 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 --- ide/wg_ProofView.ml | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'ide/wg_ProofView.ml') diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 1a333ff16..8c7aeeb8c 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -129,13 +129,13 @@ let display mode (view : #GText.view_skel) goals hints evars = match goals with | None -> () (* No proof in progress *) - | Some { Interface.fg_goals = []; Interface.bg_goals = bg; shelved_goals = shelf } -> + | Some { Interface.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } -> let bg = flatten (List.rev bg) in let evars = match evars with None -> [] | Some evs -> evs in - begin match (bg, shelf, evars) with - | [], [], [] -> + begin match (bg, shelved_goals,given_up_goals, evars) with + | [], [], [], [] -> view#buffer#insert "No more subgoals." - | [], [], _ :: _ -> + | [], [], [], _ :: _ -> (* A proof has been finished, but not concluded *) view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n"; let iter evar = @@ -143,15 +143,23 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert msg in List.iter iter evars - | [], _, _ -> + | [], [], _, _ -> + (* The proof is finished, with the exception of given up goals. *) + view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n"; + let iter goal = + let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in + view#buffer#insert msg + in + List.iter iter given_up_goals + | [], _, _, _ -> (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; let iter goal = let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in view#buffer#insert msg in - List.iter iter shelf - | _, _, _ -> + List.iter iter shelved_goals + | _, _, _, _ -> (* No foreground proofs, but still unfocused ones *) view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; let iter goal = -- cgit v1.2.3