diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:39:06 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:39:06 +0200 |
| commit | 335f219436fd1106884a0f135826a53f01801728 (patch) | |
| tree | 6a9cf62e450a6962a50dbb3262386fce6529f28e /doc | |
| parent | 48e2ccee3614503dfbc18edf5ae8f1f230927d1a (diff) | |
| parent | 479ba134a1af676b7b8f3f60c3709761fd0d0b51 (diff) | |
Merge PR #943: Reference Manual: minor wording improvements
Diffstat (limited to 'doc')
| -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 71977d3e9..ef12fe416 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 eca3efcdd..2b9e4e605 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. |