diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index e027794f81..24ff5793c0 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1025,6 +1025,15 @@ including those under binders. \ErrMsg \errindex{No evars} +\subsection{\tt is\_var \term +\tacindex{is\_var} +\label{isvar}} + +This tactic applies to any goal. It checks whether its argument is a +variable or hypothesis in the current goal context or in the opened sections. + +\ErrMsg \errindex{Not a variable or hypothesis} + \subsection{Bindings list \index{Binding list} \label{Binding-list}} |