diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 28 | ||||
| -rw-r--r-- | library/lib.mli | 1 |
2 files changed, 0 insertions, 29 deletions
diff --git a/library/lib.ml b/library/lib.ml index b98ad41104..54087ce1c0 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -573,25 +573,6 @@ let reset_to_gen test = let reset_to sp = reset_to_gen (fun x -> fst x = sp) -(* LEM: TODO - * We will need to muck with frozen states in after, too! - * Not only FrozenState, but also those embedded in Opened(Section|Module) - *) -let delete_gen test = - let (after,equal,before) = split_lib_gen test in - let rec chop_at_dot = function - | [] as l -> l - | (_, Leaf o)::t when object_tag o = "DOT" -> t - | _::t -> chop_at_dot t - and chop_before_dot = function - | [] as l -> l - | (_, Leaf o)::t as l when object_tag o = "DOT" -> l - | _::t -> chop_before_dot t - in - set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before)) - -let delete sp = delete_gen (fun x -> fst x = sp) - let reset_name (loc,id) = let (sp,_) = try @@ -601,15 +582,6 @@ let reset_name (loc,id) = in reset_to sp -let remove_name (loc,id) = - let (sp,_) = - try - find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi) - with Not_found -> - user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry") - in - delete sp - let is_mod_node = function | OpenedModule _ | OpenedSection _ | ClosedModule _ | ClosedSection _ -> true diff --git a/library/lib.mli b/library/lib.mli index 0a445f0766..df931f060f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -155,7 +155,6 @@ val close_section : unit -> unit val reset_to : Libnames.object_name -> unit val reset_name : Names.identifier Pp.located -> unit -val remove_name : Names.identifier Pp.located -> unit val reset_mod : Names.identifier Pp.located -> unit (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of |