diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-28 15:41:39 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-28 15:41:39 +0000 |
| commit | d556fd3ffb8b59e2a5136ab748a3a8d73c3f45f0 (patch) | |
| tree | df77fe692c2176defbb5414b2448af9e243cd08b /library/lib.mli | |
| parent | 76f02a4751c3eac40d91dfa7bb61de1f985672d3 (diff) | |
Cleaning backtracking code, optimized "Backtrack n x y" when n is
current state.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/library/lib.mli b/library/lib.mli index 52e6b7bd7..5639ffed7 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -65,8 +65,14 @@ val add_anonymous_leaf : obj -> unit val add_leaves : identifier -> obj list -> object_name val add_frozen_state : unit -> unit + +(* 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()]. That is it forgets the label and anything + registered after it. *) val reset_label : int -> unit (*s The function [contents_after] returns the current library segment, |