aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-23 20:12:57 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-23 20:12:57 +0100
commit62ce0d1ec197d70a81faf12e151a3da618b2d1ba (patch)
treefab23723694bc14cbf775a0bc6791df08083645c /doc
parent530cd175c1b7465c3fa35c300f42b022bed9b25b (diff)
parent347827ef4ea72048762c1677f37cb716109a5d9c (diff)
Merge PR#433: doc: fix a French-ism
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-syn.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 61093709e..ecaf82806 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -120,7 +120,7 @@ Notation "A \/ B" := (or A B) (at level 85, right associativity).
By default, a notation is considered non associative, but the
precedence level is mandatory (except for special cases whose level is
-canonical). The level is either a number or the mention {\tt next
+canonical). The level is either a number or the phrase {\tt next
level} whose meaning is obvious. The list of levels already assigned
is on Figure~\ref{init-notations}.