diff options
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 580eec8dc3..00cf4984dc 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -107,3 +107,13 @@ val emacs_str : string -> string -> string (* Backwards compatibility *) val prterm : constr -> std_ppcmds (* = pr_lconstr *) + +type printer_pr = { + pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds; + pr_subgoal : int -> goal list -> std_ppcmds; + pr_goal : goal -> std_ppcmds; +};; + +val set_printer_pr : printer_pr -> unit + +val default_printer_pr : printer_pr |