Notations: A step in cleaning constr_entry_key.

- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions

2 files changed, 20 insertions, 12 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ae7364052..42329d03a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -93,16 +93,28 @@ open Decl_kinds
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
-  let pr_set_entry_type = function
+  let pr_at_level = function
+    | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+    | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+
+  let pr_set_entry_type pr = function
     | ETName -> str"ident"
     | ETReference -> str"global"
-    | ETPattern _ -> str"pattern"
-    | ETConstr _ -> str"constr"
+    | ETPattern None -> str"pattern"
+    | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+    | ETConstr lev -> str"constr" ++ pr lev
     | ETOther (_,e) -> str e
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
 
+  let pr_at_level_opt = function
+    | None -> mt ()
+    | Some n -> spc () ++ pr_at_level n
+
+  let pr_set_simple_entry_type =
+    pr_set_entry_type pr_at_level_opt
+
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s
@@ -359,17 +371,13 @@ open Decl_kinds
   let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
 
   let pr_syntax_modifier = function
-    | SetItemLevel (l,NextLevel) ->
-      prlist_with_sep sep_v2 str l ++
-        spc() ++ keyword "at next level"
-    | SetItemLevel (l,NumLevel n) ->
-      prlist_with_sep sep_v2 str l ++
-        spc() ++ keyword "at level" ++ spc() ++ int n
-    | SetLevel n -> keyword "at level" ++ spc() ++ int n
+    | SetItemLevel (l,n) ->
+      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
+    | SetLevel n -> pr_at_level (NumLevel n)
     | SetAssoc LeftA -> keyword "left associativity"
     | SetAssoc RightA -> keyword "right associativity"
     | SetAssoc NonA -> keyword "no associativity"
-    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
     | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing -> keyword "only parsing"
     | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 5e0cc8da5..603be6308 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,7 +9,7 @@
 (** This module implements pretty-printers for vernac_expr syntactic
     objects and their subcomponents. *)
 
-val pr_set_entry_type : ('a,'b) Extend.constr_entry_key_gen -> Pp.t
+val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
 
 (** Prints a fixpoint body *)
 val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t