aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-13 14:44:27 +0200
committerEnrico Tassi2019-05-13 14:44:27 +0200
commit34fbc9cc6b30fc8e7dc2bd37756d5ede29074de0 (patch)
treec59e91fc8ad41df8e5bd4280c44cc6da3cd20ffa /interp/constrintern.ml
parentcfecef471c706beb50d70b951b148c9629a4064a (diff)
parent4895bf8bb5d0acfaee499991973fc6537657427d (diff)
Merge PR #10076: [Canonical structures] Annotation to field declarations to prevent them from being “canonical”
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c0801067ce..f06493b374 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer =
let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch.")
- | (_, regular) :: proj_kinds ->
+ | { Recordops.pk_true_proj = regular } :: proj_kinds ->
(* "regular" is false when the field is defined
by a let-in in the record declaration
(its value is fixed from other fields). *)