diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b82cdc2d..450d3b2d 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -989,6 +989,36 @@ Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals have names of the form {\ident}\texttt{\_admitted} possibly followed by a number. +\subsection{\tt constr\_eq \term$_1$ \term$_2$ +\tacindex{constr\_eq} +\label{constreq}} + +This tactic applies to any goal. It checks whether its arguments are +equal modulo alpha conversion and casts. + +\ErrMsg \errindex{Not equal} + +\subsection{\tt is\_evar \term +\tacindex{is\_evar} +\label{isevar}} + +This tactic applies to any goal. It checks whether its argument is an +existential variable. Existential variables are uninstantiated +variables generated by e.g. {\tt eapply} (see Section~\ref{apply}). + +\ErrMsg \errindex{Not an evar} + +\subsection{\tt has\_evar \term +\tacindex{has\_evar} +\label{hasevar}} + +This tactic applies to any goal. It checks whether its argument has an +existential variable as a subterm. Unlike {\tt context} patterns +combined with {\tt is\_evar}, this tactic scans all subterms, +including those under binders. + +\ErrMsg \errindex{No evars} + \subsection{Bindings list \index{Binding list} \label{Binding-list}} @@ -3917,7 +3947,7 @@ where {\sl hint\_definition} is one of the following expressions: \begin{quotation} \begin{verbatim} -Hint Extern 4 ~(?=?) => discriminate. +Hint Extern 4 (~(_ = _)) => discriminate. \end{verbatim} \end{quotation} @@ -4294,7 +4324,7 @@ Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 13344 2010-07-28 15:04:36Z msozeau $ +% $Id: RefMan-tac.tex 13659 2010-11-29 11:09:07Z glondu $ %%% Local Variables: %%% mode: latex |