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

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e38da45b95..418e13759b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -295,7 +295,7 @@ let tag_var = tag Tag.variable
       | CPatOr pl ->
         hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
 
-      | CPatNotation ("( _ )",([p],[]),[]) ->
+      | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
         pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
 
       | CPatNotation (s,(l,ll),args) ->
@@ -665,7 +665,7 @@ let tag_var = tag Tag.variable
                     | CastCoerce -> str ":>"),
           lcast
         )
-      | CNotation ("( _ )",([t],[],[],[])) ->
+      | CNotation ((_,"( _ )"),([t],[],[],[])) ->
         return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
       | CNotation (s,env) ->
         pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env