diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-12-06 17:52:26 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-12-06 17:52:26 +0100 |
| commit | 227ff6a46ad511ff2ab0ba1ffb9017bdb0291a58 (patch) | |
| tree | 7ff1074927231c65cf4a9c139a1fcbb94607ffd3 /doc/refman/RefMan-tac.tex | |
| parent | 7c1c1a71d57cbe5d8543789592b5df21d6fe31e1 (diff) | |
Update documentation (bugs #5246 and #5251).
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 01dc1dec9..4b0652031 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -302,7 +302,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}. \begin{ErrMsgs} -\item \errindex{Impossible to unify \dots\ with \dots} +\item \errindex{Unable to unify \dots\ with \dots} The {\tt apply} tactic failed to match the conclusion of {\term} and the current goal. @@ -4621,7 +4621,7 @@ It is equivalent to {\tt apply refl\_equal}. \begin{ErrMsgs} \item \errindex{The conclusion is not a substitutive equation} -\item \errindex{Impossible to unify \dots\ with \dots} +\item \errindex{Unable to unify \dots\ with \dots} \end{ErrMsgs} \subsection{\tt symmetry} |