diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |