summaryrefslogtreecommitdiff
path: root/engine/nameops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/nameops.mli')
-rw-r--r--engine/nameops.mli44
1 files changed, 0 insertions, 44 deletions
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 96842dfb..8a93fad8 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -94,47 +94,3 @@ end
(** Metavariables *)
val pr_meta : Constr.metavariable -> Pp.t
val string_of_meta : Constr.metavariable -> string
-
-val out_name : Name.t -> Id.t
-[@@ocaml.deprecated "Same as [Name.get_id]"]
-
-val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-[@@ocaml.deprecated "Same as [Name.fold_right]"]
-
-val name_iter : (Id.t -> unit) -> Name.t -> unit
-[@@ocaml.deprecated "Same as [Name.iter]"]
-
-val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.map]"]
-
-val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-[@@ocaml.deprecated "Same as [Name.fold_left_map]"]
-
-val name_max : Name.t -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.pick]"]
-
-val name_cons : Name.t -> Id.t list -> Id.t list
-[@@ocaml.deprecated "Same as [Name.cons]"]
-
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "Same as [Name.print]"]
-
-val pr_id : Id.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Id.print]"]
-
-val pr_lab : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Label.print]"]
-
-(** Deprecated stuff to libnames *)
-val default_library : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_library]"]
-
-val coq_root : module_ident (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_root]"]
-
-val coq_string : string (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_string]"]
-
-val default_root_prefix : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]
-