diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index e6eaccb3f8..a409d61bb8 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -701,11 +701,11 @@ Notation}. % Introduction An {\em interpretation scope} is a set of notations for terms with -their interpretation. Interpretation scopes provides with a weak, -purely syntactical form of notations overloading: a same notation, for -instance the infix symbol \verb=+= can be used to denote distinct -definitions of an additive operator. Depending on which interpretation -scopes is currently open, the interpretation is different. +their interpretation. Interpretation scopes provide a weak, +purely syntactical form of notation overloading: the same notation, for +instance the infix symbol \verb=+=, can be used to denote distinct +definitions of the additive operator. Depending on which interpretation +scope is currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the {\ocaml} level. |