aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppconstr.mli')
-rw-r--r--printing/ppconstr.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 34cccfc2d..be96cfce5 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -60,6 +60,7 @@ val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
val pr_constr_expr : constr_expr -> Pp.t
val pr_lconstr_expr : constr_expr -> Pp.t
val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
+val pr_constr_expr_n : tolerability -> constr_expr -> Pp.t
type term_pr = {
pr_constr_expr : constr_expr -> Pp.t;