aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 102c6ef6d..4d7a71631 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