From 4dbf44a47949adce5e538a7aacc670ec64c28d3f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 12 Jan 2016 10:39:49 +0100
Subject: restore documentation of admit

---
 doc/refman/RefMan-tac.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d90a027295..11d62b60a3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1468,6 +1468,24 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
+\subsection{\tt admit}
+\tacindex{admit}
+\tacindex{give\_up}
+\label{admit}
+
+The {\tt admit} tactic allows temporarily skipping a subgoal so as to
+progress further in the rest of the proof.  A proof containing
+admitted goals cannot be closed with {\tt Qed} but only with
+{\tt Admitted}.
+
+\begin{Variants}
+
+  \item {\tt give\_up}
+
+    Synonym of {\tt admit}.
+
+\end{Variants}
+
 \subsection{\tt absurd \term}
 \tacindex{absurd}
 \label{absurd}
-- 
cgit v1.2.3