From 61df4fc36bfc8b2fadbcf8db9751cefde8c75a93 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 1 Nov 2003 22:16:21 +0000 Subject: 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 --- interp/coqlib.ml | 10 ++++++++-- interp/coqlib.mli | 1 + 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 -- cgit v1.2.3