diff options
author | 2010-12-02 09:24:33 +0000 | |
---|---|---|
committer | 2010-12-02 09:24:33 +0000 | |
commit | 64a5d7b33c4c66fc82974f255cf40badd0b7bacf (patch) | |
tree | d4b9f0c5beb36a98a3a8868ae5c13545b54d4644 /doc/refman/RefMan-tac.tex | |
parent | a281f908a65ba7ba0678f42e20b3a0ed78250b18 (diff) |
Add tactic has_evar (#2433)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13664 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
-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 3f9f03c40..40954f83e 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}} |