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.

1 files changed, 25 insertions, 0 deletions

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5ecfaf590c..bda5774abf 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