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
---
 lib/interface.mli | 2 ++
 lib/serialize.ml  | 8 +++++---
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/interface.mli b/lib/interface.mli
index d190272569..31577e6296 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -46,6 +46,8 @@ type goals = {
   (** Zipper representing the unfocussed background goals *)
   shelved_goals : goal list;
   (** List of the goals on the shelf. *)
+  given_up_goals : goal list;
+  (** List of the goals that have been given up *)
 }
 
 type hint = (string * string) list
diff --git a/lib/serialize.ml b/lib/serialize.ml
index f3c06d9306..743247faf6 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -259,14 +259,16 @@ let of_goals g =
   let fg = of_list of_goal g.fg_goals in
   let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
   let shelf = of_list of_goal g.shelved_goals in
-  Element ("goals", [], [fg; bg; shelf])
+  let given_up = of_list of_goal g.given_up_goals in
+  Element ("goals", [], [fg; bg; shelf; given_up])
 let to_goals = function
-  | Element ("goals", [], [fg; bg; shelf]) ->
+  | Element ("goals", [], [fg; bg; shelf; given_up]) ->
     let to_glist = to_list to_goal in
     let fg = to_list to_goal fg in
     let bg = to_list (to_pair to_glist to_glist) bg in
     let shelf = to_list to_goal shelf in
-    { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; }
+    let given_up = to_list to_goal given_up in
+    { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up }
   | _ -> raise Marshal_error
 
 let of_coq_info info =
-- 
cgit v1.2.3