diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /printing/ppconstr.mli | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'printing/ppconstr.mli')
| -rw-r--r-- | printing/ppconstr.mli | 2 |
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 |