aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:14 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-05 16:47:14 +0000
commit4c65f9a13758e5378026de77cfe5600e2dae8a73 (patch)
treeb91e79c1433a70e4596a9ca0946b522b62e04357 /library
parentac2ca408aef1759e4682d989a40ab332068edcdb (diff)
Lib: remove strange code about backtracking to the current state
We now forbid a "BackTo n" or "Backtrack n _ _" when n is the current label or a future one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14453 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml19
-rw-r--r--library/lib.mli6
2 files changed, 12 insertions, 13 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 904824dc1..f6b25e201 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -659,17 +659,16 @@ let is_label_n n x =
| (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true
| _ -> false
-(* Reset the label registered by [mark_end_of_command()] with number n. *)
+(** Reset the label registered by [mark_end_of_command()] with number n,
+ which should be strictly in the past. *)
+
let reset_label n =
- let current = current_command_label() in
- if n < current then
- let res = reset_to_gen (is_label_n n) in
- set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
- res
- else (* optimisation to avoid recaching when not necessary (why is it so long??) *)
- match !lib_stk with
- | [] -> ()
- | x :: ls -> (lib_stk := ls;set_command_label (n-1))
+ if n >= current_command_label () then
+ error "Cannot backtrack to the current label or a future one";
+ let res = reset_to_gen (is_label_n n) in
+ (* forget state numbers after n only if reset succeeded *)
+ set_command_label (n-1);
+ res
let rec back_stk n stk =
match stk with
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 ... } *)