aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-08 19:11:28 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 19:27:09 +0100
commit4d9375d18d58958d992f76799ad545b800321d78 (patch)
tree72e7665d8efe27e64ebf27da5ef2df850b4536d1 /CHANGES
parent5542ffe43dde333cec6d118fd4b0424313330c33 (diff)
Revert "Merge PR #873: New strategy based on open scopes for deciding which notation to use among several of them"
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 0 insertions, 4 deletions
diff --git a/CHANGES b/CHANGES
index 320b325ae..1ed110b4b 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