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.

1 files changed, 3 insertions, 1 deletions

diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 6d9effcef4..942ea5ff3f 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -58,6 +58,8 @@ type tmp_scope_name = scope_name
 
 type subscopes = tmp_scope_name option * scope_name list
 
+type extended_subscopes = Constrexpr.notation_entry_level * subscopes
+
 (** 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  *)
 
@@ -86,7 +88,7 @@ type notation_var_internalization_type =
 
 (** This characterizes to what a notation is interpreted to *)
 type interpretation =
-    (Id.t * (subscopes * notation_var_instance_type)) list *
+    (Id.t * (extended_subscopes * notation_var_instance_type)) list *
     notation_constr
 
 type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list