Extending further PR#6047 (system to register printers for Ltac values).

We generalize the possible use of levels to raw and glob printers.

This is potentially useful for printing ltac expressions which are the
glob level.

8 files changed, 220 insertions, 115 deletions

diff --git a/API/API.mli b/API/API.mli
index 1f1b05ead..2aa5da67d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5217,16 +5217,20 @@ end
 
 module Genprint :
 sig
-  type printer_with_level =
+  type 'a with_level =
     { default_already_surrounded : Notation_term.tolerability;
       default_ensure_surrounded : Notation_term.tolerability;
-      printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+      printer : 'a }
   type printer_result =
-    | PrinterBasic of (unit -> Pp.t)
-    | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-    | PrinterNeedsContextAndLevel of printer_with_level
-  type 'a printer = 'a -> Pp.t
-  type 'a top_printer = 'a -> printer_result
+| PrinterBasic of (unit -> Pp.t)
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+  type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+  type top_printer_result =
+    | TopPrinterBasic of (unit -> Pp.t)
+    | TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+    | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+  type 'a printer = 'a -> printer_result
+  type 'a top_printer = 'a -> top_printer_result
   val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
                         'raw printer -> 'glb printer -> 'top top_printer -> unit
   val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type ->
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4b9e0fff4..6aa2f6f89 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -84,6 +84,24 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> Pp.t) ->
     'a -> Pp.t
 
+type 'a raw_extra_genarg_printer_with_level =
+    (constr_expr -> Pp.t) ->
+    (constr_expr -> Pp.t) ->
+    (tolerability -> raw_tactic_expr -> Pp.t) ->
+    tolerability -> 'a -> Pp.t
+
+type 'a glob_extra_genarg_printer_with_level =
+    (glob_constr_and_expr -> Pp.t) ->
+    (glob_constr_and_expr -> Pp.t) ->
+    (tolerability -> glob_tactic_expr -> Pp.t) ->
+    tolerability -> 'a -> Pp.t
+
+type 'a extra_genarg_printer_with_level =
+    (EConstr.constr -> Pp.t) ->
+    (EConstr.constr -> Pp.t) ->
+    (tolerability -> Val.t -> Pp.t) ->
+    tolerability -> 'a -> Pp.t
+
 let string_of_genarg_arg (ArgumentType arg) =
   let rec aux : type a b c. (a, b, c) genarg_type -> string = function
   | ListArg t -> aux t ^ "_list"
@@ -127,9 +145,9 @@ let string_of_genarg_arg (ArgumentType arg) =
           | Some Refl ->
              let open Genprint in
              match generic_top_print (in_gen (Topwit wit) x) with
-             | PrinterBasic pr -> pr ()
-             | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty
-             | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+             | TopPrinterBasic pr -> pr ()
+             | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
                 printer (Global.env()) Evd.empty default_ensure_surrounded
           end
         | _ -> default
@@ -1194,42 +1212,77 @@ let declare_extra_genarg_pprule wit
     | ExtraArg s -> ()
     | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
   end;
-  let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+  let f x =
+    Genprint.PrinterBasic (fun () ->
+        f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   let g x =
+    Genprint.PrinterBasic (fun () ->
     let env = Global.env () in
-    g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x
+    g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x)
   in
   let h x =
-    Genprint.PrinterNeedsContext (fun env sigma ->
+    Genprint.TopPrinterNeedsContext (fun env sigma ->
         h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
   in
   Genprint.register_print0 wit f g h
 
+let declare_extra_genarg_pprule_with_level wit
+  (f : 'a raw_extra_genarg_printer_with_level)
+  (g : 'b glob_extra_genarg_printer_with_level)
+  (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded =
+  begin match wit with
+    | ExtraArg s -> ()
+    | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
+  end;
+  let open Genprint in
+  let f x =
+    PrinterNeedsLevel {
+        default_already_surrounded = default_surrounded;
+        default_ensure_surrounded = default_non_surrounded;
+        printer = (fun n ->
+          f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in
+  let g x =
+    let env = Global.env () in
+    PrinterNeedsLevel {
+        default_already_surrounded = default_surrounded;
+        default_ensure_surrounded = default_non_surrounded;
+        printer = (fun n ->
+          g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) }
+  in
+  let h x =
+    TopPrinterNeedsContextAndLevel {
+        default_already_surrounded = default_surrounded;
+        default_ensure_surrounded = default_non_surrounded;
+        printer = (fun env sigma n ->
+          h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) }
+  in
+  Genprint.register_print0 wit f g h
+
 let declare_extra_vernac_genarg_pprule wit f =
-  let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
+  let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   Genprint.register_vernac_print0 wit f
 
 (** Registering *)
 
-let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma ->
+let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma ->
   let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in
   Miscprint.pr_intro_pattern print_constr p)
 
-let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma ->
+let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma ->
   pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
                pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
 
-let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
   let sigma, bl = bl env sigma in
   Miscprint.pr_bindings
     (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
 
-let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma ->
+let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
   let sigma, bl = bl env sigma in
   pr_with_bindings
     (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
 
-let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
+let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma ->
   let sigma, c = match c with
   | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c)
   | clear_flag,ElimOnAnonHyp n as x -> sigma, x
@@ -1238,12 +1291,16 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
     (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
 
 let make_constr_printer f c =
-  Genprint.PrinterNeedsContextAndLevel {
+  Genprint.TopPrinterNeedsContextAndLevel {
       Genprint.default_already_surrounded = Ppconstr.ltop;
       Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
       Genprint.printer = (fun env sigma n -> f env sigma n c)}
 
 let lift f a = Genprint.PrinterBasic (fun () -> f a)
+let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a)
+
+let register_basic_print0 wit f g h =
+  Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
 
 let pr_glob_constr_pptac c =
@@ -1257,80 +1314,81 @@ let pr_lglob_constr_pptac c =
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
-  Genprint.register_print0 wit_int_or_var
-    (pr_or_var int) (pr_or_var int) (lift int);
-  Genprint.register_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global);
-  Genprint.register_print0 wit_ident
-    pr_id pr_id (lift pr_id);
-  Genprint.register_print0 wit_var
-    (pr_located pr_id) (pr_located pr_id) (lift pr_id);
-  Genprint.register_print0
+  let open Genprint in
+  register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
+  register_basic_print0 wit_ref
+    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+  register_basic_print0 wit_ident pr_id pr_id pr_id;
+  register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id;
+  register_print0
     wit_intro_pattern
-    (Miscprint.pr_intro_pattern pr_constr_expr)
-    (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c))
+    (lift (Miscprint.pr_intro_pattern pr_constr_expr))
+    (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c)))
     pr_intro_pattern_env;
   Genprint.register_print0
     wit_clause_dft_concl
-    (pr_clauses (Some true) pr_lident)
-    (pr_clauses (Some true) pr_lident)
-    (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
+    (lift (pr_clauses (Some true) pr_lident))
+    (lift (pr_clauses (Some true) pr_lident))
+    (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
   ;
   Genprint.register_print0
     wit_constr
-    Ppconstr.pr_constr_expr
-    (fun (c, _) -> pr_glob_constr_pptac c)
+    (lift Ppconstr.pr_lconstr_expr)
+    (lift (fun (c, _) -> pr_lglob_constr_pptac c))
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_uconstr
-    Ppconstr.pr_constr_expr
-    (fun (c, _) -> pr_glob_constr_pptac c)
+    (lift Ppconstr.pr_constr_expr)
+    (lift (fun (c,_) -> pr_glob_constr_pptac c))
     (make_constr_printer Printer.pr_closed_glob_n_env)
   ;
   Genprint.register_print0
     wit_open_constr
-    Ppconstr.pr_constr_expr
-    (fun (c, _) -> pr_glob_constr_pptac c)
+    (lift Ppconstr.pr_constr_expr)
+    (lift (fun (c, _) -> pr_glob_constr_pptac c))
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
-  Genprint.register_print0 wit_red_expr
-    (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
-    (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))
+  Genprint.register_print0
+    wit_red_expr
+    (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)))
+    (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)))
     pr_red_expr_env
   ;
-  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
-  Genprint.register_print0 wit_bindings
-    (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
-    (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
+  register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+  register_print0 wit_bindings
+    (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr))
+    (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
     pr_bindings_env
   ;
-  Genprint.register_print0 wit_constr_with_bindings
-    (pr_with_bindings pr_constr_expr pr_lconstr_expr)
-    (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
+  register_print0 wit_constr_with_bindings
+    (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr))
+    (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
     pr_with_bindings_env
   ;
-  Genprint.register_print0 wit_open_constr_with_bindings
-    (pr_with_bindings pr_constr_expr pr_lconstr_expr)
-    (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
+  register_print0 wit_open_constr_with_bindings
+    (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr))
+    (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
     pr_with_bindings_env
   ;
-  Genprint.register_print0 Tacarg.wit_destruction_arg
-    (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
-    (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
+  register_print0 Tacarg.wit_destruction_arg
+    (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr))
+    (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
     pr_destruction_arg_env
   ;
-  Genprint.register_print0 Stdarg.wit_int int int (lift int);
-  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool);
-  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit);
-  Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str);
-  Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring)
+  register_basic_print0 Stdarg.wit_int int int int;
+  register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
+  register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
+  register_basic_print0 Stdarg.wit_pre_ident str str str;
+  register_basic_print0 Stdarg.wit_string qstring qstring qstring
 
 let () =
-  let printer _ _ prtac = prtac (0, E) in
-  declare_extra_genarg_pprule wit_tactic printer printer printer
+  let printer _ _ prtac = prtac in
+  declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
+  ltop (0,E)
 
 let () =
-  let pr_unit _ _ _ () = str "()" in
-  let printer _ _ prtac = prtac (0, E) in
-  declare_extra_genarg_pprule wit_ltac printer printer pr_unit
+  let pr_unit _ _ _ _ () = str "()" in
+  let printer _ _ prtac = prtac in
+  declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit
+  ltop (0,E)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5ecfaf590..bda5774ab 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -40,12 +40,37 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> Pp.t) ->
     'a -> Pp.t
 
+type 'a raw_extra_genarg_printer_with_level =
+    (constr_expr -> Pp.t) ->
+    (constr_expr -> Pp.t) ->
+    (tolerability -> raw_tactic_expr -> Pp.t) ->
+    tolerability -> 'a -> Pp.t
+
+type 'a glob_extra_genarg_printer_with_level =
+    (glob_constr_and_expr -> Pp.t) ->
+    (glob_constr_and_expr -> Pp.t) ->
+    (tolerability -> glob_tactic_expr -> Pp.t) ->
+    tolerability -> 'a -> Pp.t
+
+type 'a extra_genarg_printer_with_level =
+    (EConstr.constr -> Pp.t) ->
+    (EConstr.constr -> Pp.t) ->
+    (tolerability -> Val.t -> Pp.t) ->
+    tolerability -> 'a -> Pp.t
+
 val declare_extra_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
   'a raw_extra_genarg_printer ->
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
+val declare_extra_genarg_pprule_with_level :
+  ('a, 'b, 'c) genarg_type ->
+  'a raw_extra_genarg_printer_with_level ->
+  'b glob_extra_genarg_printer_with_level ->
+  'c extra_genarg_printer_with_level ->
+  (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit
+
 val declare_extra_vernac_genarg_pprule :
   ('a, 'b, 'c) genarg_type ->
   'a raw_extra_genarg_printer -> unit
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index c03a86732..9ae112d37 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -33,7 +33,7 @@ let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_bin
   let () = register_val0 wit None in
   let () = Genprint.register_val_print0 (base_val_typ wit)
              (fun c ->
-               Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
+               Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
   wit
 
 (** All the types considered here are base types *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 1a8ec6d6f..8df23b14e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
   let wit = Genarg.create_arg "tacvalue" in
   let () = register_val0 wit None in
   let () = Genprint.register_val_print0 (base_val_typ wit)
-             (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in
+             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
   wit
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
@@ -242,9 +242,9 @@ let pr_value env v =
     | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
   let open Genprint in
   match generic_val_print v with
-  | PrinterBasic pr -> pr ()
-  | PrinterNeedsContext pr -> pr_with_env pr
-  | PrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+  | TopPrinterBasic pr -> pr ()
+  | TopPrinterNeedsContext pr -> pr_with_env pr
+  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
      pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
 
 let pr_closure env ist body =
@@ -821,9 +821,9 @@ let message_of_value v =
     Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in
   let open Genprint in
   match generic_val_print v with
-  | PrinterBasic pr -> Ftactic.return (pr ())
-  | PrinterNeedsContext pr -> pr_with_env pr
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+  | TopPrinterBasic pr -> Ftactic.return (pr ())
+  | TopPrinterNeedsContext pr -> pr_with_env pr
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
      pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded)
 
 let interp_message_token ist = function
@@ -1353,8 +1353,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         begin
           let open Genprint in
           match generic_val_print v with
-          | PrinterBasic _ -> call_debug None
-          | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ ->
+          | TopPrinterBasic _ -> call_debug None
+          | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ ->
              Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl)))
         end <*>
         if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 776a212b5..37a94fe21 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -16,21 +16,27 @@ open Geninterp
 
 (* Printing generic values *)
 
-type printer_with_level =
+type 'a with_level =
   { default_already_surrounded : Notation_term.tolerability;
     default_ensure_surrounded : Notation_term.tolerability;
-    printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+    printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsContextAndLevel of printer_with_level
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
 
-type 'a printer = 'a -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
 
-type 'a top_printer = 'a -> printer_result
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
 
-module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end)
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
+
+module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end)
 
 let print0_val_map = ref ValMap.empty
 
@@ -48,32 +54,32 @@ let register_val_print0 s pr =
   print0_val_map := ValMap.add s pr !print0_val_map
 
 let combine_dont_needs pr_pair pr1 = function
-  | PrinterBasic pr2 ->
-     PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
-  | PrinterNeedsContext pr2 ->
-     PrinterNeedsContext (fun env sigma ->
+  | TopPrinterBasic pr2 ->
+     TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ()))
+  | TopPrinterNeedsContext pr2 ->
+     TopPrinterNeedsContext (fun env sigma ->
          pr_pair (pr1 ()) (pr2 env sigma))
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-     PrinterNeedsContext (fun env sigma ->
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     TopPrinterNeedsContext (fun env sigma ->
          pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded))
 
 let combine_needs pr_pair pr1 = function
-  | PrinterBasic pr2 ->
-     PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
-  | PrinterNeedsContext pr2 ->
-     PrinterNeedsContext (fun env sigma ->
+  | TopPrinterBasic pr2 ->
+     TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ()))
+  | TopPrinterNeedsContext pr2 ->
+     TopPrinterNeedsContext (fun env sigma ->
          pr_pair (pr1 env sigma) (pr2 env sigma))
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-     PrinterNeedsContext (fun env sigma ->
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+     TopPrinterNeedsContext (fun env sigma ->
          pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded))
 
 let combine pr_pair pr1 v2 =
   match pr1 with
-  | PrinterBasic pr1 ->
+  | TopPrinterBasic pr1 ->
      combine_dont_needs pr_pair pr1 (generic_val_print v2)
-  | PrinterNeedsContext pr1 ->
+  | TopPrinterNeedsContext pr1 ->
      combine_needs pr_pair pr1 (generic_val_print v2)
-  | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+  | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
      combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded)
        (generic_val_print v2)
 
@@ -81,14 +87,14 @@ let _ =
   let pr_cons a b = Pp.(a ++ spc () ++ b) in
   register_val_print0 Val.typ_list
     (function
-     | [] -> PrinterBasic mt
+     | [] -> TopPrinterBasic mt
      | a::l ->
         List.fold_left (combine pr_cons) (generic_val_print a) l)
 
 let _ =
   register_val_print0 Val.typ_opt
     (function
-     | None -> PrinterBasic Pp.mt
+     | None -> TopPrinterBasic Pp.mt
      | Some v -> generic_val_print v)
 
 let _ =
@@ -99,9 +105,9 @@ let _ =
 (* Printing generic arguments *)
 
 type ('raw, 'glb, 'top) genprinter = {
-  raw : 'raw printer;
-  glb : 'glb printer;
-  top : 'top -> printer_result;
+  raw : 'raw -> printer_result;
+  glb : 'glb -> printer_result;
+  top : 'top -> top_printer_result;
 }
 
 module PrintObj =
@@ -112,9 +118,9 @@ struct
   | ExtraArg tag ->
     let name = ArgT.repr tag in
     let printer = {
-      raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
-      glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
-      top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
+      top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">"));
     } in
     Some printer
   | _ -> assert false
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 2da9bbc36..baa60fcb2 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -10,19 +10,25 @@
 
 open Genarg
 
-type printer_with_level =
+type 'a with_level =
   { default_already_surrounded : Notation_term.tolerability;
     default_ensure_surrounded : Notation_term.tolerability;
-    printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t }
+    printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsContextAndLevel of printer_with_level
+| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
 
-type 'a printer = 'a -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
 
-type 'a top_printer = 'a -> printer_result
+type top_printer_result =
+| TopPrinterBasic of (unit -> Pp.t)
+| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t)
+| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level
+
+type 'a printer = 'a -> printer_result
+
+type 'a top_printer = 'a -> top_printer_result
 
 val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer
 (** Printer for raw level generic arguments. *)
@@ -34,7 +40,7 @@ val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer
 (** Printer for top level generic arguments. *)
 
 val register_print0 : ('raw, 'glb, 'top) genarg_type ->
-  'raw printer -> 'glb printer -> ('top -> printer_result) -> unit
+  'raw printer -> 'glb printer -> 'top top_printer -> unit
 val register_val_print0 : 'top Geninterp.Val.typ ->
   'top top_printer -> unit
 val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type ->
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 12d5338ad..a544b4762 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -130,7 +130,10 @@ let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
       let q = in_gen (rawwit wit2) q in
       hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
     | ExtraArg s ->
-      Genprint.generic_raw_print (in_gen (rawwit wit) x)
+       let open Genprint in
+       match generic_raw_print (in_gen (rawwit wit) x) with
+       | PrinterBasic pp -> pp ()
+       | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
 
 
 let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
@@ -152,4 +155,7 @@ let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
       let ans = pr_sequence (pr_glb_generic env) [p; q] in
       hov_if_not_empty 0 ans
     | ExtraArg s ->
-      Genprint.generic_glb_print (in_gen (glbwit wit) x)
+       let open Genprint in
+       match generic_glb_print (in_gen (glbwit wit) x) with
+       | PrinterBasic pp -> pp ()
+       | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded