diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 3f9f03c40f..40954f83ed 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -999,6 +999,17 @@ 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}} |