diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli index d80822056d..438754a381 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -82,6 +82,7 @@ val make_path : identifier -> section_path (* Kernel-side names *) val current_prefix : unit -> module_path * dir_path val make_kn : identifier -> kernel_name +val make_con : identifier -> constant (* Are we inside an opened section *) val sections_are_opened : unit -> bool |