From f963cf312d5a8ebb84af92489be5efd49fe6f434 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Wed, 2 Apr 2014 11:18:13 +0200
Subject: Better error message when found more than once object of name ...

---
 interp/coqlib.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index bf5b7db417..bf5d225b2c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -58,10 +58,12 @@ let gen_constant_in_modules locstr dirs s =
 	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
 	prlist_with_sep pr_comma pr_dirpath dirs)
     | l ->
-	anomaly ~label:locstr
-	(str ("found more than once object of name "^s^
-	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
-	prlist_with_sep pr_comma pr_dirpath dirs)
+      anomaly ~label:locstr
+	(str ("ambiguous name "^s^" can represent ") ++
+	   prlist_with_sep pr_comma
+	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
+	   str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	   prlist_with_sep pr_comma pr_dirpath dirs)
 
 
 (* For tactics/commands requiring vernacular libraries *)
-- 
cgit v1.2.3