diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 69710f431..2d5d5258f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -141,3 +141,9 @@ val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc + +(* popping one level of section in global names *) + +val pop_con : constant -> constant +val pop_kn : kernel_name -> kernel_name +val pop_global_reference : global_reference -> global_reference |