From 60daf674df3d11fa2948bbc7c9a928c09f22d099 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 17:19:49 +0100
Subject: Adding support for custom entries in notations.

- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
  entries. This typically corresponds to rules of the form
  'Notation "[ x ]" := x (x custom myconstr).' but also
  'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
  are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
  are natively recognized.

Incidentally merging ETConstr and ETConstrAsBinder.

Noticed in passing that parsing binder as custom was not done as in
constr.

Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
---
 parsing/extend.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'parsing/extend.ml')

diff --git a/parsing/extend.ml b/parsing/extend.ml
index f57e32c884..a3e27f9cf5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -38,10 +38,8 @@ type 'a constr_entry_key_gen =
   | ETReference
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
-  | ETConstr of 'a
-  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
+  | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
-  | ETOther of string * string
 
 (** Entries level (left-hand side of grammar rules) *)
 
@@ -63,9 +61,8 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
+  | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
-  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
   | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
   | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
 
-- 
cgit v1.2.3


From 90a1d7202182205b3a66b4e8edf751e82b117551 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 29 Jun 2018 08:28:27 +0200
Subject: Renaming ETName and ETReference so as to fit the user-visible
 terminology.

ETName -> ETIdent
ETReference -> ETGlobal
---
 parsing/extend.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/extend.ml')

diff --git a/parsing/extend.ml b/parsing/extend.ml
index a3e27f9cf5..6fe2956643 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -34,8 +34,8 @@ type production_level =
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
-  | ETName
-  | ETReference
+  | ETIdent
+  | ETGlobal
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
-- 
cgit v1.2.3