From 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 14:23:11 +0200
Subject: More precise explanation when a notation is not reversible for
 printing.

---
 intf/notation_term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index cad6f4b821..d1cbb6a33d 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -74,7 +74,7 @@ type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
 
-type reversibility_flag = bool
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
 
 type notation_interp_env = {
   ninterp_var_type : notation_var_internalization_type Id.Map.t;
-- 
cgit v1.2.3


From 51976c9f2157953f794ed1efcd68403a8545d346 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Aug 2017 13:58:59 +0200
Subject: A bit of miscellaneous code documentation around notations.

---
 intf/notation_term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index d1cbb6a33d..028d14ccfd 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -63,7 +63,7 @@ type subscopes = tmp_scope_name option * scope_name list
 type notation_var_instance_type =
   | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
 
-(** Type of variables when interpreting a constr_expr as an notation_constr:
+(** Type of variables when interpreting a constr_expr as a notation_constr:
     in a recursive pattern x..y, both x and y carry the individual type
     of each element of the list x..y *)
 type notation_var_internalization_type =
-- 
cgit v1.2.3


From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Aug 2017 20:05:03 +0200
Subject: Allows recursive patterns for binders to be associative on the left.

This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.

Example of (artificial) notation that this commit supports:

  Notation "! x .. y # A #" :=
    (.. (A,(forall x, True)) ..,(forall y, True))
    (at level 200, x binder).
---
 intf/notation_term.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 028d14ccfd..52fd0f368f 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -25,11 +25,11 @@ type notation_constr =
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
-  | NList of Id.t * Id.t * notation_constr * notation_constr * bool
+  | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
-  | NBinderList of Id.t * Id.t * notation_constr * notation_constr
+  | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of Constr.case_style * notation_constr option *
       (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
-- 
cgit v1.2.3


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.
---
 intf/notation_term.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 52fd0f368f..83cc454f43 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -61,13 +61,13 @@ type subscopes = tmp_scope_name option * scope_name list
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
 type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList
+  | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList
 
 (** Type of variables when interpreting a constr_expr as a notation_constr:
     in a recursive pattern x..y, both x and y carry the individual type
     of each element of the list x..y *)
 type notation_var_internalization_type =
-  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
+  | NtnInternTypeAny | NtnInternTypeOnlyBinder
 
 (** This characterizes to what a notation is interpreted to *)
 type interpretation =
@@ -95,7 +95,7 @@ type precedence = int
 type parenRelation = L | E | Any | Prec of precedence
 type tolerability = precedence * parenRelation
 
-type level = precedence * tolerability list * notation_var_internalization_type list
+type level = precedence * tolerability list * Extend.constr_entry_key list
 
 (** Grammar rules for a notation *)
 
-- 
cgit v1.2.3


From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 12:35:56 +0200
Subject: Respecting the ident/pattern distinction in notation modifiers.

---
 intf/notation_term.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 83cc454f43..0f4bfef600 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -60,8 +60,11 @@ type subscopes = tmp_scope_name option * scope_name list
 
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
+
+type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern
+
 type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList
+  | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
 
 (** Type of variables when interpreting a constr_expr as a notation_constr:
     in a recursive pattern x..y, both x and y carry the individual type
-- 
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}.
---
 intf/notation_term.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 0f4bfef600..86f5adbd78 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -61,7 +61,14 @@ type subscopes = tmp_scope_name option * scope_name list
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
 
-type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern
+type notation_binder_source =
+  (* This accepts only pattern *)
+  (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
+  | NtnParsedAsPattern of bool
+  (* This accepts only ident *)
+  | NtnParsedAsIdent
+  (* This accepts ident, or pattern, or both *)
+  | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
 
 type notation_var_instance_type =
   | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
-- 
cgit v1.2.3