diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index aaa2ee51f..ae3d8fe04 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -535,6 +535,11 @@ in the list of subgoals remaining to prove. This tactic behaves like \texttt{assert ({\ident} : {\form})}. +\item \texttt{pose proof {\term} as {\ident}} + + This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where + \texttt{T} is the type of {\term}. + \end{Variants} % PAS CLAIR; @@ -1275,6 +1280,10 @@ last introduced hypothesis. {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of {\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}. +\item \texttt{pose proof {\term} as {\intropattern}} + + This tactic behaves like \texttt{destruct {\term} as {\intropattern}}. + \item{\tt destruct {\term} using {\qualid}} This is a synonym of {\tt induction {\term} using {\qualid}}. |