diff options
| author | Pierre-Marie Pédrot | 2018-10-06 13:55:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-06 13:55:48 +0200 |
| commit | 371566f7619aed79aad55ffed6ee0920b961be6e (patch) | |
| tree | f5a7f56d5d5e924987ef0970aa0b72ec53aad673 /kernel/names.mli | |
| parent | 28df7dd06dbea299736f3897ecabd2a6e3fd8e28 (diff) | |
| parent | 650c65af484c45f4e480252b55d148bcc198be6c (diff) | |
Merge PR #8555: Remove section paths from kernel names
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 2ea8108734..2145a51c4e 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 |