diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index c1d6b1d0c9..3f9f03c40f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -989,6 +989,16 @@ Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals have names of the form {\ident}\texttt{\_admitted} possibly followed by a number. +\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{Bindings list \index{Binding list} \label{Binding-list}} |