Optimisation de gen_constant_in_modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4689 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 10 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index c9852e8a53..a381c35e16 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -40,16 +40,20 @@ let list_try_find f =
 let gen_constant_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let id = Constrextern.id_of_v7_string s in
-  try
-    list_try_find
-      (fun dir ->
-	constr_of_reference
-	  (Nametab.absolute_reference (Libnames.make_path dir id)))
-      dirs
-  with Not_found ->
-    anomalylabstrm "" (str (locstr^": cannot find "^s^
-    " in module"^(if List.length dirs > 1 then "s " else " ")) ++
-    prlist_with_sep pr_coma pr_dirpath dirs)
+  let all = Nametab.locate_all (make_short_qualid id) in
+  let these =
+    List.filter (fun r -> List.mem (dirpath (sp_of_global r)) dirs) all in
+  match these with
+    | [x] -> constr_of_reference x
+    | [] ->
+	anomalylabstrm "" (str (locstr^": cannot find "^s^
+	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	prlist_with_sep pr_coma pr_dirpath dirs)
+    | l ->
+	anomalylabstrm "" 
+	(str (locstr^": found more than once object of name "^s^
+	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	prlist_with_sep pr_coma pr_dirpath dirs)
 
 let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s