Merge branch 'v8.5'

2 files changed, 1 insertions, 13 deletions

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}