diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 12 |
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} |