aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.mli')
-rw-r--r--library/lib.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/library/lib.mli b/library/lib.mli
index 8defad867..419f91317 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -68,9 +68,9 @@ val mark_end_of_command : unit -> unit
(** Returns the current label number *)
val current_command_label : unit -> int
-(** [reset_label n ] resets [lib_stk] to the label n registered by
- [mark_end_of_command()]. That is it forgets the label and anything
- registered after it. *)
+(** [reset_label n] resets [lib_stk] to the label n registered by
+ [mark_end_of_command()]. It forgets the label and anything
+ registered after it. The label should be strictly in the past. *)
val reset_label : int -> unit
(** {6 ... } *)