aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 23:08:55 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 23:08:55 +0100
commit020c3448cc71618c3e74f64ae6217113072d1bbd (patch)
tree0f4a7d4282730eb397c64be13ba10e14c465283a /CHANGES
parent1f2a922d52251f79a11d75c2205e6827a07e591b (diff)
parent4d9375d18d58958d992f76799ad545b800321d78 (diff)
Merge PR #6949: Revert PR #873: New strategy based on open scopes for deciding…
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