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

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 5bf46282fd..ccad6b19eb 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -167,7 +167,7 @@ let dump_modref ?loc mp ty =
 let dump_libref ?loc dp ty =
   dump_ref ?loc (Names.DirPath.to_string dp) "<>" "<>" ty
 
-let cook_notation df sc =
+let cook_notation (from,df) sc =
   (* We encode notations so that they are space-free and still human-readable *)
   (* - all spaces are replaced by _                                           *)
   (* - all _ denoting a non-terminal symbol are replaced by x                 *)
@@ -203,7 +203,9 @@ let cook_notation df sc =
     if !i <= l then (set ntn !j '_'; incr j; incr i)
   done;
   let df = Bytes.sub_string ntn 0 !j in
-  match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+  let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
+  let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+  from_df_sc
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
   if dump () then