diff options
| -rw-r--r-- | library/lib.ml | 28 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
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 |