diff options
| author | Guillaume Melquiond | 2016-12-06 17:52:26 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-12-26 10:11:41 +0100 |
| commit | aad7ca30a093190be17ac504b8a36cb04ae928de (patch) | |
| tree | 64349259339d34bf0d168fb4528ec10f77d5fe12 | |
| parent | dd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 (diff) | |
Update documentation (bugs #5246 and #5251).
| -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 fcccd9cb4b..5880b6c848 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -711,9 +711,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 11de4f35e0..d539af7e31 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -292,7 +292,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. @@ -4593,7 +4593,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} |