aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.mli
diff options
context:
space:
mode:
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 ce37c3614..bca419c9a 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