diff options
| author | Gaëtan Gilbert | 2019-05-23 10:54:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 09:55:51 +0200 |
| commit | 1c5e2508d6a9604ffd77eff3140a86eafbc672a9 (patch) | |
| tree | 2a93d48b0dd438db2b936e3cbbfe322f2140604f /interp/constrintern.ml | |
| parent | 82663b28a04d82e89bd041efd256c4838312e587 (diff) | |
Fix #10225 (Instance := {} accepts duplicate fields)
This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.
Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4c8aff3f2e..63c936fa81 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1299,7 +1299,7 @@ let find_pattern_variable qid = if qualid_is_ident qid then qualid_basename qid else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) -let check_duplicate loc fields = +let check_duplicate ?loc fields = let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with @@ -1344,7 +1344,7 @@ let sort_fields ~complete loc fields completer = try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in - let () = check_duplicate loc fields in + let () = check_duplicate ?loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) |