aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-06-11 15:14:15 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-07-27 10:10:23 +0200
commite3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch)
treea9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /printing/ppconstr.ml
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index cf513321f..ee03bc900 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -731,10 +731,10 @@ let tag_var = tag Tag.variable
(sep() ++ if prec_less prec inherited then strm else surround strm)
type term_pr = {
- pr_constr_expr : constr_expr -> std_ppcmds;
- pr_lconstr_expr : constr_expr -> std_ppcmds;
- pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
- pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+ pr_constr_expr : constr_expr -> Pp.t;
+ pr_lconstr_expr : constr_expr -> Pp.t;
+ pr_constr_pattern_expr : constr_pattern_expr -> Pp.t;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
}
type precedence = Ppextend.precedence * Ppextend.parenRelation