Remove undocumented command "Delete foo"

 This command isn't trivial to port to the forthcoming evolution of
 backtracking in coqtop. Moreover, it isn't clear whether this
 "Delete" works well in advanced situation (was not updating
 frozen states).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15084 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 0 insertions, 29 deletions

diff --git a/library/lib.ml b/library/lib.ml
index b98ad4110..54087ce1c 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 0a445f076..df931f060 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