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, 8 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a78e3448ea..88a16e014c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4626,7 +4626,7 @@ back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
 
     Shelves only these goals under focused which are mentioned in other goals.
     Goals which appear in the type of other goals can be solve by unification.
-    
+
 \Example
 \begin{coq_example}
 Goal exists n, n=0.
@@ -4646,6 +4646,13 @@ Reset Initial.
 This command moves all the goals on the shelf (see Section~\ref{shelve}) from the
 shelf into focus, by appending them to the end of the current list of focused goals.
 
+\subsection[\tt give\_up]{\tt give\_up\tacindex{give\_up}}
+
+This tactic removes the focused goals from the proof. They are not solved, and cannot
+be solved later in the proof. As the goals are not solved, the proof cannot be closed.
+
+The {\tt give\_up} tactic can be used while editing a proof, to choose to write the
+proof script in a non-sequential order.
 
 \section{Simple tactic macros}
 \index{Tactic macros}