diff options
| author | Gabriel Scherer | 2015-06-30 18:06:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 12:57:30 +0200 |
| commit | c83fa10156545bce96ef4a0f93e8695ec353c834 (patch) | |
| tree | 975b5bd65022c9a88a1fe1622c89a292bbc076fc | |
| parent | c11b7c5a34ea16a32a78c796a219d29edd117e74 (diff) | |
minor: comment on the meaning of the 'boolean' variable
| -rw-r--r-- | interp/constrintern.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 56a191262c..5c5a900fba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1081,11 +1081,10 @@ let sort_fields ~complete loc fields completer = begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch") | (_, 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). *) if first_field && not regular && complete then - (* G.S.: why do we fail only in the - first-field case? I would expect to fail - whenever (not regular && complete), and - skip the fields only when (not complete *) user_err_loc (loc, "", str "No local fields allowed in a record construction.") else if first_field then build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc |