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, 11 insertions, 10 deletions

diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index d2b50fa83d..e1f5e20117 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -11,6 +11,7 @@
 open Util
 open Pp
 open CErrors
+open Notation
 open Notation_gram
 
 (*s Pretty-print. *)
@@ -48,29 +49,29 @@ type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
 let notation_rules =
-  Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
+  Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
 
 let declare_notation_rule ntn ~extra unpl gram =
-  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+  notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules
 
 let find_notation_printing_rule ntn =
-  try pi1 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
+  try pi1 (NotationMap.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
 let find_notation_extra_printing_rules ntn =
-  try pi2 (String.Map.find ntn !notation_rules)
+  try pi2 (NotationMap.find ntn !notation_rules)
   with Not_found -> []
 let find_notation_parsing_rules ntn =
-  try pi3 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
+  try pi3 (NotationMap.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
 
 let get_defined_notations () =
-  String.Set.elements @@ String.Map.domain !notation_rules
+  NotationSet.elements @@ NotationMap.domain !notation_rules
 
 let add_notation_extra_printing_rule ntn k v =
   try
     notation_rules :=
-      let p, pp, gr = String.Map.find ntn !notation_rules in
-      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
+      let p, pp, gr = NotationMap.find ntn !notation_rules in
+      NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules
   with Not_found ->
     user_err ~hdr:"add_notation_extra_printing_rule"
       (str "No such Notation.")