diff options
author | 2010-12-02 09:24:31 +0000 | |
---|---|---|
committer | 2010-12-02 09:24:31 +0000 | |
commit | a281f908a65ba7ba0678f42e20b3a0ed78250b18 (patch) | |
tree | 269e09b6faf1dcb43bfd97f1f64451ad9557e33a /doc/refman | |
parent | 75ed3a811a215a2a4130cb58970588c42879bbd8 (diff) |
Add tactic is_evar (Closes: #2433)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13663 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
-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 c1d6b1d0c..3f9f03c40 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}} |