aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 0 insertions, 4 deletions
diff --git a/CHANGES b/CHANGES
index 63913bff5..441154b3a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,10 +7,6 @@ Notations
right (e.g. "( x ; .. ; y ; z )") now supported.
- Notations with a specific level for the leftmost nonterminal,
when printing-only, are supported.
-- When several notations are available for the same expression,
- priority is given to latest notations defined in the scopes being
- opened rather than to the latest notations defined independently of
- whether they are in an opened scope or not.
- Notations can now refer to the syntactic category of patterns (as in
"fun 'pat =>" or "match p with pat => ... end"). Two variants are
available, depending on whether a single variable is considered as a