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.
---
 interp/constrexpr.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 521eeb8e96..d8dd4ef6dd 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -20,7 +20,10 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
-type notation = string
+type notation_entry = InConstrEntry | InCustomEntry of string
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_key = string
+type notation = notation_entry_level * notation_key
 
 type 'a or_by_notation_r =
   | AN of 'a
-- 
cgit v1.2.3