diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 3738aa94aa..f773d60c55 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1041,13 +1041,6 @@ end = struct (* {{{ *) | `Stop x -> x | `Cont acc -> next acc - let back_safe () = - let id = - fold_until (fun n (id,_,_,_,_) -> - if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n)) - 0 (VCS.get_branch_pos (VCS.current_branch ())) in - backto id - let undo_vernac_classifier v = try match v with |