diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/API/API.mli b/API/API.mli index 6227f17c6..abbdf22b9 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5247,16 +5247,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 -> |