From 6e4c4578044c15ec172009a570d13b9e168cb93e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 28 Jan 2017 19:02:20 +0100
Subject: Fix bug #5262: Error should tell me which name is duplicated.

---
 toplevel/record.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index ef09f6fa54..b8dcf81fde 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -550,8 +550,10 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (List.distinct_f Id.compare allnames)
-  then error "Two objects have the same name";
+  let () = match List.duplicates Id.equal allnames with
+  | [] -> ()
+  | id :: _ -> errorlabstrm "" (str "Two objects have the same name" ++ spc () ++ quote (Id.print id))
+  in
   let isnot_class = match kind with Class false -> false | _ -> true in
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";
-- 
cgit v1.2.3