aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Valentin Robert <valentin.robert.42@gmail.com>2017-02-16 14:37:47 -0800
committerGravatar Valentin Robert <valentin.robert.42@gmail.com>2017-03-14 22:15:40 -0700
commit347827ef4ea72048762c1677f37cb716109a5d9c (patch)
tree0cc9e62c674cd967daa5b780e85698c244f76f50 /doc
parentbcb634d070519d6e37d9b7d39f12437a7d38f0c2 (diff)
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 21c39de96..ce662eb20 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -114,7 +114,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}.