diff options
| -rw-r--r-- | printing/ppconstr.ml | 1 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 9 |
2 files changed, 4 insertions, 6 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 102c6ef6de..4d7a716319 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -738,7 +738,6 @@ let tag_var = tag Tag.variable pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } - type precedence = Notation_term.precedence * Notation_term.parenRelation let modular_constr_pr = pr let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 7546c748d8..34cccfc2d0 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -86,9 +86,8 @@ val default_term_pr : term_pr Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) -type precedence -val lsimpleconstr : precedence -val ltop : precedence +val lsimpleconstr : tolerability +val ltop : tolerability val modular_constr_pr : - ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) -> - (unit->Pp.t) -> precedence -> constr_expr -> Pp.t + ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t |