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 | |
| parent | 7c1c1a71d57cbe5d8543789592b5df21d6fe31e1 (diff) | |
Update documentation (bugs #5246 and #5251).
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 99eee44e0..3814e4403 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -713,9 +713,9 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ & & \\ -{\inductivebody} & ::= & - {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\ - && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\ +{\inductivebody} & ::= & + {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\ + && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\ & & \\ %% TODO: where ... %% Fixpoints {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ 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} |