diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 01:42:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-02 01:42:29 +0200 |
| commit | 109e05059692d0f2f15a4b1699ff4a25d07e5a79 (patch) | |
| tree | 4cc5a8a736fcbe978ca990f0b1a61143e594d1cd /interp/constrintern.ml | |
| parent | acbe712fd643516ff63ecfe3e106deb695dbd9b3 (diff) | |
Fix bug #5087: Improve the error message on record with duplicated fields.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4502aa7ac..f98873aa6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1061,6 +1061,15 @@ let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) +let check_duplicate loc fields = + let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in + let dups = List.duplicates eq fields in + match dups with + | [] -> () + | (r, _) :: _ -> + user_err_loc (loc, "", str "This record defines several times the field " ++ + pr_reference r ++ str ".") + (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1094,6 +1103,7 @@ let sort_fields ~complete loc fields completer = try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) with Not_found -> anomaly (str "Environment corruption for records") 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 *) |