diff options
| author | aspiwack | 2013-11-02 15:40:19 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:40:19 +0000 |
| commit | fb1c2f25fb0ca5f422c69e14b6b434ad1d8f01a9 (patch) | |
| tree | 37629e2fd9a96a6eee0ffbbe8d7daf4dca9e7650 /toplevel | |
| parent | bd39dfc9d8090f50bff6260495be2782e6d5e342 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_slave.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 48afe324ec..a519b58816 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -193,7 +193,7 @@ let goals () = if not (String.is_empty s) then msg_info (str s); try let pfts = Proof_global.give_me_the_proof () in - let (goals, zipper, shelf, sigma) = Proof.proof pfts in + let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in let fg = List.map (process_goal sigma) goals in let map_zip (lg, rg) = let lg = List.map (process_goal sigma) lg in @@ -202,7 +202,11 @@ let goals () = in let bg = List.map map_zip zipper in let shelf = List.map (process_goal sigma) shelf in - Some { Interface.fg_goals = fg; Interface.bg_goals = bg; shelved_goals = shelf; } + let given_up = List.map (process_goal sigma) given_up in + Some { Interface.fg_goals = fg; + Interface.bg_goals = bg; + shelved_goals = shelf; + given_up_goals = given_up; } with Proof_global.NoCurrentProof -> None let evars () = |