diff options
| -rw-r--r-- | pretyping/termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index a1d07777b2..6cf9b4e0db 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -865,4 +865,6 @@ let construct_reference ctx id = with Not_found -> global_reference id +let global_reference_in_absolute_module dir id = + constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id)) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9c9243c8c7..9031ec42de 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -180,6 +180,7 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr +val global_reference_in_absolute_module : dir_path -> identifier -> constr (* Test if an identifier is the basename of a global reference *) val is_global : identifier -> bool |