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

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 ... } *)