diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 19 | ||||
| -rw-r--r-- | library/lib.mli | 3 |
2 files changed, 3 insertions, 19 deletions
diff --git a/library/lib.ml b/library/lib.ml index f6b25e201d..cfaea3b663 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -553,13 +553,6 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false -let has_top_frozen_state () = - let rec aux = function - | (sp, FrozenState _)::_ -> Some sp - | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t - | _ -> None - in aux !lib_stk - let set_lib_stk new_lib_stk = lib_stk := new_lib_stk; recalc_path_prefix (); @@ -579,14 +572,6 @@ let reset_to_gen test = let reset_to sp = reset_to_gen (fun x -> fst x = sp) -let reset_to_state sp = - let (_,eq,before) = split_lib sp in - (* if eq a frozen state, we'll reset to it *) - match eq with - | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f - | _ -> error "Not a frozen state" - - (* LEM: TODO * We will need to muck with frozen states in after, too! * Not only FrozenState, but also those embedded in Opened(Section|Module) @@ -677,7 +662,9 @@ let rec back_stk n stk = | _::tail -> back_stk n tail | [] -> error "Reached begin of command history" -let back n = reset_to (back_stk n !lib_stk) +let back n = + reset_to (back_stk n !lib_stk); + set_command_label (current_command_label () - n - 1) (* State and initialization. *) diff --git a/library/lib.mli b/library/lib.mli index 419f913176..0d6eb34b87 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -157,9 +157,6 @@ val reset_to : Libnames.object_name -> unit val reset_name : Names.identifier Util.located -> unit val remove_name : Names.identifier Util.located -> unit val reset_mod : Names.identifier Util.located -> unit -val reset_to_state : Libnames.object_name -> unit - -val has_top_frozen_state : unit -> Libnames.object_name option (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of [mark_end_of_command] (counting backwards) *) |