diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/nametab.ml | 3 | ||||
-rwxr-xr-x | library/nametab.mli | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index ac6c61116..5bb21b3e5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -419,12 +419,13 @@ let locate_mind qid = | TrueGlobal (IndRef (kn,0)) -> kn | _ -> raise Not_found - let absolute_reference sp = match SpTab.find sp !the_ccitab with | TrueGlobal ref -> ref | _ -> raise Not_found +let extended_absolute_reference sp = SpTab.find sp !the_ccitab + let locate_in_absolute_module dir id = absolute_reference (make_path dir id) diff --git a/library/nametab.mli b/library/nametab.mli index eab86db1d..225a8b080 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -116,9 +116,10 @@ val locate_module : qualid -> module_path (* A variant looking up a [section_path] *) val absolute_reference : section_path -> global_reference +val extended_absolute_reference : section_path -> extended_global_reference -(*s These function tell if the given absolute name is already taken *) +(*s These functions tell if the given absolute name is already taken *) val exists_cci : section_path -> bool val exists_modtype : section_path -> bool |