Fix bug #5262: Error should tell me which name is duplicated.

1 files 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";