diff options
author | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
commit | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch) | |
tree | b04b45d1a6f42d19b1428c522d647afbad2f9b83 /doc/refman/RefMan-tac.tex | |
parent | 3e96002677226c0cdaa8f355938a76cfb37a722a (diff) |
Imported Upstream version 8.3pl1upstream/8.3pl1
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 |