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, 5 insertions, 5 deletions

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index f038b5be1a..58fa221b16 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,18 +53,18 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const
 exception No_match
 
 val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
-      ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list *
-      ('a cases_pattern_disjunction_g * subscopes) list *
-      ('a extended_glob_local_binder_g list * subscopes) list
+      ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
+      ('a cases_pattern_disjunction_g * extended_subscopes) list *
+      ('a extended_glob_local_binder_g list * extended_subscopes) list
 
 val match_notation_constr_cases_pattern :
   'a cases_pattern_g -> interpretation ->
-  (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+  (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
     (int * 'a cases_pattern_g list)
 
 val match_notation_constr_ind_pattern :
   inductive -> 'a cases_pattern_g list -> interpretation ->
-  (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) *
+  (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
     (int * 'a cases_pattern_g list)
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)