diff options
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 68a2e5dace..0d628ac7ee 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -900,7 +900,7 @@ These are synonyms of the {\tt Definition} forms. \end{Variants} \begin{ErrMsgs} -\item \errindex{Error: The term {\term} has type {\type} while it is expected to have type {\type}} +\item \errindex{The term {\term} has type {\type} while it is expected to have type {\type}} \end{ErrMsgs} \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}. |