Merge branch 'v8.5'

3 files changed, 2 insertions, 14 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 5a66910722..589933578a 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1465,7 +1465,7 @@ You can use the {\tt Clear} command.
 \Question{How can use a proof which is not finished?}
 
 You can use the {\tt Admitted} command to state your current proof as an axiom.
-You can use the {\tt admit} tactic to omit a portion of a proof.
+You can use the {\tt give\_up} tactic to omit a portion of a proof.
 
 \Question{How can I state a conjecture?}
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 32f94abf7a..556a2dab58 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -432,7 +432,7 @@ the search results via the command
 {\tt Add Search Blacklist "substring1"}.
 A lemma whose fully-qualified name contains any of the declared substrings
 will be removed from the search results.
-The default blacklisted substrings are {\tt "\_admitted"
+The default blacklisted substrings are {\tt 
   "\_subproof" "Private\_"}. The command {\tt Remove Search Blacklist
   ...} allows expunging this blacklist.
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 52f32d0c7d..2eebac18e6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1439,18 +1439,6 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
-\subsection{\tt admit}
-\tacindex{admit}
-\label{admit}
-
-The {\tt admit} tactic ``solves'' the current subgoal by an
-axiom. This typically allows temporarily skipping a subgoal so as to
-progress further in the rest of the proof. To know if some proof still
-relies on unproved subgoals, one can use the command {\tt Print
-Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
-have names of the form {\ident}\texttt{\_admitted} possibly followed
-by a number.
-
 \subsection{\tt absurd \term}
 \tacindex{absurd}
 \label{absurd}