diff options
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-int.tex | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 71977d3e9d..ef12fe416a 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -37,7 +37,7 @@ Similarly, the notation ``\nelist{\entry}{}'' stands for a non empty sequence of expressions parsed by the ``{\entry}'' entry, without any separator between. -At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a +Finally, the notation ``\sequence{\entry}{\tt sep}'' stands for a possibly empty sequence of expressions parsed by the ``{\entry}'' entry, separated by the literal ``{\tt sep}''. diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index eca3efcdd6..2b9e4e6051 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -58,7 +58,7 @@ Chapter~\ref{Addoc-coqide}. \section*{How to read this book} -This is a Reference Manual, not a User Manual, then it is not made for a +This is a Reference Manual, not a User Manual, so it is not made for a continuous reading. However, it has some structure that is explained below. |