diff options
Diffstat (limited to 'printing/pputils.ml')
| -rw-r--r-- | printing/pputils.ml | 10 |
1 files changed, 8 insertions, 2 deletions
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 |