diff options
Diffstat (limited to 'printing/pputils.mli')
-rw-r--r-- | printing/pputils.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/printing/pputils.mli b/printing/pputils.mli index 06123362a..6039168f8 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -39,3 +39,9 @@ val pr_red_expr_env : Environ.env -> Evd.evar_map -> val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t + +(* The comments interface is imperative due to the printer not + threading it, this could be solved using a better data + structure. *) +val beautify_comments : ((int * int) * string) list ref +val extract_comments : int -> string list |