diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 32 |
1 files changed, 9 insertions, 23 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 2ea8108734..98995752a2 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -274,9 +274,11 @@ sig type t (** Constructor and destructor *) - val make : ModPath.t -> DirPath.t -> Label.t -> t + val make : ModPath.t -> Label.t -> t + val repr : t -> ModPath.t * Label.t + val make2 : ModPath.t -> Label.t -> t - val repr : t -> ModPath.t * DirPath.t * Label.t + [@@ocaml.deprecated "Please use [KerName.make]"] (** Projections *) val modpath : t -> ModPath.t @@ -317,15 +319,12 @@ sig val make2 : ModPath.t -> Label.t -> t (** Shortcut for [(make1 (KerName.make2 ...))] *) - val make3 : ModPath.t -> DirPath.t -> Label.t -> t - (** Shortcut for [(make1 (KerName.make ...))] *) - (** Projections *) val user : t -> KerName.t val canonical : t -> KerName.t - val repr3 : t -> ModPath.t * DirPath.t * Label.t + val repr2 : t -> ModPath.t * Label.t (** Shortcut for [KerName.repr (user ...)] *) val modpath : t -> ModPath.t @@ -403,15 +402,12 @@ sig val make2 : ModPath.t -> Label.t -> t (** Shortcut for [(make1 (KerName.make2 ...))] *) - val make3 : ModPath.t -> DirPath.t -> Label.t -> t - (** Shortcut for [(make1 (KerName.make ...))] *) - (** Projections *) val user : t -> KerName.t val canonical : t -> KerName.t - val repr3 : t -> ModPath.t * DirPath.t * Label.t + val repr2 : t -> ModPath.t * Label.t (** Shortcut for [KerName.repr (user ...)] *) val modpath : t -> ModPath.t @@ -531,15 +527,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool (** equalities on constant and inductive names (for the checker) *) -val eq_con_chk : Constant.t -> Constant.t -> bool -[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."] - val eq_ind_chk : inductive -> inductive -> bool -(** {6 Deprecated functions. For backward compatibility.} *) - -type mod_bound_id = MBId.t -[@@ocaml.deprecated "Same as [MBId.t]."] (** {5 Module paths} *) type module_path = ModPath.t = @@ -619,6 +608,9 @@ module Projection : sig val hcons : t -> t (** Hashconsing of projections. *) + val repr_equal : t -> t -> bool + (** Ignoring the unfolding boolean. *) + val compare : t -> t -> int val map : (MutInd.t -> MutInd.t) -> t -> t @@ -629,9 +621,6 @@ module Projection : sig end -type projection = Projection.t -[@@ocaml.deprecated "Alias for [Projection.t]"] - (** {6 Global reference is a kernel side type for all references together } *) (* XXX: Should we define GlobRefCan GlobRefUser? *) @@ -669,9 +658,6 @@ module GlobRef : sig end -type global_reference = GlobRef.t -[@@ocaml.deprecated "Alias for [GlobRef.t]"] - (** Better to have it here that in Closure, since required in grammar.cma *) (* XXX: Move to a module *) type evaluable_global_reference = |