diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/library/lib.mli b/library/lib.mli index a956ff5d0..04f8d0775 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -147,31 +147,6 @@ val remove_section_part : Globnames.global_reference -> Names.DirPath.t val open_section : Names.Id.t -> unit val close_section : unit -> unit -(** {6 Backtracking } *) - -(** NB: The next commands are low-level ones, do not use them directly - otherwise the command history stack in [Backtrack] will be out-of-sync. - Also note that [reset_initial] is now [reset_label first_command_label] *) - -(** Adds a "dummy" entry in lib_stk with a unique new label number. *) -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()]. It forgets anything registered after - this label. The label should be strictly in the past. *) -val reset_label : int -> unit - -(** [raw_reset_initial] is now [reset_label] to the first label. - This is meant to be used during initial Load's and compilations. - Otherwise, consider instead [Backtrack.reset_initial] *) -val raw_reset_initial : unit -> unit - -(** search the label registered immediately before adding some definition *) -val label_before_name : Names.Id.t Loc.located -> int - (** {6 We can get and set the state of the operations (used in [States]). } *) type frozen |