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, 3 deletions

diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 8ce0316f53..989a6c5bf1 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -217,8 +217,8 @@ let interp_search_notation ?loc tag okey =
          (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
       else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
     loop 0 1 in
-  let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in
-  let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in
+  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+  let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
   let pr_and_list pr = function
     | [x] -> pr x
     | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
@@ -293,7 +293,7 @@ let interp_search_notation ?loc tag okey =
     let scs' = List.remove (=) sc !scs in
     let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
     Feedback.msg_warning (hov 4 w)
-  else if String.string_contains ~where:ntn ~what:" .. " then
+  else if String.string_contains ~where:(snd ntn) ~what:" .. " then
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function