From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 09:15:40 +0200
Subject: Adding support for parsing subterms of a notation as "pattern".

This allows in particular to define notations with 'pat style binders.

E.g.:

A non-trivial change in this commit is storing binders and patterns
separately from terms.

This is not strictly necessary but has some advantages.

However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).

So, it is as simple to always store idents (and eventually patterns)
as terms.
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 8d344d4f09..8fa69fd7ad 100644
--- a/CHANGES
+++ b/CHANGES
@@ -11,6 +11,8 @@ Notations
   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").
 
 Specification language
 
-- 
cgit v1.2.3


From 149997b59c6711c551490c4e7601eaac59f5f675 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 19:51:45 +0200
Subject: A first step at refreshing and documenting the new feature.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 8fa69fd7ad..d597bf7a6a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,6 +13,9 @@ Notations
   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").
+- 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.
 
 Specification language
 
-- 
cgit v1.2.3


From b176959335a8cc097c254ea10b910e8ecbcde54b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 24 Aug 2017 21:14:43 +0200
Subject: More flexibility in locating or referring to a notation.

We generalize the possibility to refer to a notation not only by its
"_ U _" form but also using its "a 'U' b".

(Wish from EJGA)
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index d597bf7a6a..74e120a316 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,6 +16,8 @@ Notations
 - 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.
+- "Locate" now working also on notations of the form "x + y" (rather
+  than "_ + _").
 
 Specification language
 
-- 
cgit v1.2.3


From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 20:50:03 +0100
Subject: 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}.
---
 CHANGES | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 74e120a316..32a533d14f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.
-- 
cgit v1.2.3