diff options
author | 2012-02-18 00:48:07 +0000 | |
---|---|---|
committer | 2012-02-18 00:48:07 +0000 | |
commit | 18e6108339aaf18499c1c64f05655f442ab100f8 (patch) | |
tree | 72d9d66ffc1a7c2960ee84472a9e45b39a119d02 /doc/refman | |
parent | 60618d500c2d32c8e85e599022ceb8cff2a220a3 (diff) |
Document the [unify] tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a8300da37..ca5be4d98 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1004,6 +1004,22 @@ equal modulo alpha conversion and casts. \ErrMsg \errindex{Not equal} +\subsection{\tt unify \term$_1$ \term$_2$ +\tacindex{unify} +\label{unify}} + +This tactic applies to any goal. It checks whether its arguments are +unifiable, potentially instantiating existential variables. + +\ErrMsg \errindex{Not unifiable} + +\begin{Variants} +\item {\tt unify \term$_1$ \term$_2$ with \ident} + + Unification takes the transparency information defined in the + hint database {\tt \ident} into account (see Section~\ref{HintTransparency}). +\end{Variants} + \subsection{\tt is\_evar \term \tacindex{is\_evar} \label{isevar}} |