aboutsummaryrefslogtreecommitdiff
path: root/printing/ppconstr.mli
diff options
context:
space:
mode:
authorEnrico Tassi2018-06-19 16:48:12 +0200
committerEnrico Tassi2018-06-19 16:48:12 +0200
commit6715e6801c1d285a12eeca55dd8b831d7efb8c0d (patch)
tree2b8925708d85f7cef5fb222d551cf809704f8ebd /printing/ppconstr.mli
parentc37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (diff)
parent133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce (diff)
Merge PR #7797: Remove reference name type.
Diffstat (limited to 'printing/ppconstr.mli')
-rw-r--r--printing/ppconstr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index ce37c3614a..bca419c9ac 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -47,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) ->
lident option * recursion_order_expr ->
Pp.t
-val pr_record_body : (reference * constr_expr) list -> Pp.t
+val pr_record_body : (qualid * constr_expr) list -> Pp.t
val pr_binders : local_binder_expr list -> Pp.t
val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t