diff options
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 61093709ec..ecaf82806e 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}. |