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

7 files changed, 0 insertions, 34 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
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9b66cacb16..38e4e8eec1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -931,7 +931,6 @@ GEXTEND Gram
 
 (* Resetting *)
       | IDENT "Reset"; id = identref -> VernacResetName id
-      | IDENT "Delete"; id = identref -> VernacRemoveName id
       | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c4ffbfd152..49c76c96ce 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -471,7 +471,6 @@ let rec pr_vernac = function
   | VernacCheckGuard -> str"Guarded"
 
   (* Resetting *)
-  | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id
   | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
   | VernacResetInitial -> str"Reset Initial"
   | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index f92dcdb084..bc024e6418 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -153,7 +153,6 @@ let rec attribute_of_vernac_command = function
   | VernacRestoreState _ -> []
 
   (* Resetting *)
-  | VernacRemoveName _ -> [NavigationCommand]
   | VernacResetName _ -> [NavigationCommand]
   | VernacResetInitial -> [NavigationCommand]
   | VernacBack _ -> [NavigationCommand]
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 12508d754e..6100fbd1dd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1511,7 +1511,6 @@ let interp c = match c with
   | VernacRestoreState s -> vernac_restore_state s
 
   (* Resetting *)
-  | VernacRemoveName id -> Lib.remove_name id
   | VernacResetName id -> vernac_reset_name id
   | VernacResetInitial -> vernac_reset_initial ()
   | VernacBack n -> vernac_back n
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d77349bc58..c017393c1b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -302,7 +302,6 @@ type vernac_expr =
   | VernacRestoreState of string
 
   (* Resetting *)
-  | VernacRemoveName of lident
   | VernacResetName of lident
   | VernacResetInitial
   | VernacBack of int