diff options
Diffstat (limited to 'library/nametab.ml')
| -rwxr-xr-x | library/nametab.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index f6418de3e..cbb3b23e9 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -355,7 +355,7 @@ let locate_module qid = | DirModule (_,(mp,_)) -> mp | _ -> raise Not_found -let locate_loaded_library qid = +let full_name_module qid = match locate_dir qid with | DirModule (dir,_) -> dir | _ -> raise Not_found @@ -428,6 +428,9 @@ let id_of_global ctx_opt ref = let sp_of_syntactic_definition kn = Globrevtab.find (SyntacticDef kn) !the_globrevtab +let dir_of_mp mp = + MPmap.find mp !the_modrevtab + (* Shortest qualid functions **********************************************) |