diff options
Diffstat (limited to 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index e110ad00a..d38ef592f 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -26,7 +26,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (id_of_string s) in - try global_of_extended_global (Nametab.extended_absolute_reference sp) + try global_of_extended_global (Nametab.extended_global_of_path sp) with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp)) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s @@ -36,7 +36,7 @@ let gen_reference = coq_reference let gen_constant = coq_constant let has_suffix_in_dirs dirs ref = - let dir = dirpath (sp_of_global ref) in + let dir = dirpath (path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let global_of_extended q = @@ -45,7 +45,7 @@ let global_of_extended q = let gen_constant_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let id = id_of_string s in - let all = Nametab.extended_locate_all (make_short_qualid id) in + let all = Nametab.locate_extended_all (qualid_of_ident id) in let all = list_uniquize (list_map_filter global_of_extended all) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with |