Controle par le prefixe et plus par le nom absolu pour la recherche d'objets dans la biblio standard

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

2 files changed, 9 insertions, 2 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index a381c35e1..914717d39 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -37,12 +37,15 @@ let list_try_find f =
   in 
   try_find_f
 
+let has_suffix_in_dirs dirs ref =
+  let dir = dirpath (sp_of_global ref) in
+  List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+
 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
   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
+  let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> constr_of_reference x
     | [] ->
@@ -59,6 +62,9 @@ let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s
 
 let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s  
 
+let arith_dir = ["Coq";"Arith"]
+let arith_modules = [arith_dir]
+
 let zarith_dir = ["Coq";"ZArith"]
 let zarith_base_modules = [
   zarith_dir@["fast_integer"];
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index cd169dbcd..658a899fb 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -27,6 +27,7 @@ val gen_constant : string->string list -> string -> constr
 
 (* Search in several modules (not prefixed by "Coq") *)
 val gen_constant_in_modules : string->string list list-> string -> constr
+val arith_modules : string list list
 val zarith_base_modules : string list list
 val init_modules : string list list