diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 20:50:03 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
commit | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (patch) | |
tree | 48bc1c2a7aef0498290e55917323dcc484e2e878 /CHANGES | |
parent | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (diff) |
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -12,7 +12,9 @@ Notations 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"). + "fun 'pat =>" or "match p with pat => ... end"). Two variants are + available, depending on whether a single variable is considered as a + pattern or not. - Recursive notations now support ".." patterns with several occurrences of the recursive term or binder, possibly mixing terms and binders, possibly in reverse left-to-right order. |