From 109e05059692d0f2f15a4b1699ff4a25d07e5a79 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 2 Oct 2016 01:42:29 +0200
Subject: Fix bug #5087: Improve the error message on record with duplicated
 fields.

---
 interp/constrintern.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4502aa7ace..f98873aa66 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 *)
-- 
cgit v1.2.3