diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index e7ee8b1a4..bac155bb5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -556,12 +556,12 @@ in the list of subgoals remaining to prove. This tactic behaves like \texttt{assert ({\ident} : {\form})}. -\item \texttt{pose proof {\term} as {\ident}} +\item \texttt{pose proof {\term} as {\ident}\tacindex{pose proof}} This tactic behaves like \texttt{assert ({\ident:T}) by exact {\term}} where \texttt{T} is the type of {\term}. -\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)} \\ +\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)\tacindex{specialize}} \\ {\tt specialize {\ident} with \bindinglist} The tactic {\tt specialize} works on local hypothesis \ident. |