diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/lib.mli b/library/lib.mli index c43155816..fa8a34344 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -66,7 +66,8 @@ val add_leaves : identifier -> obj list -> object_name val add_frozen_state : unit -> unit val mark_end_of_command : unit -> unit - +val current_command_label : unit -> int +val reset_label : int -> unit (*s The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment |