diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 07:42:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 23:26:19 +0100 |
| commit | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (patch) | |
| tree | 73ce61804aae0e16b1a30994affd75a59ed08efe /API | |
| parent | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (diff) | |
[api] Miscellaneous consolidation + moves to engine.
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index 86c6f1415..991dca748 100644 --- a/API/API.mli +++ b/API/API.mli @@ -87,6 +87,7 @@ sig val repr : t -> Id.t list val equal : t -> t -> bool val to_string : t -> string + val print : t -> Pp.t end module MBId : sig @@ -1934,8 +1935,10 @@ sig val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t val dirpath_of_string : string -> Names.DirPath.t val pr_dirpath : Names.DirPath.t -> Pp.t + [@@ocaml.deprecated "Alias for DirPath.print"] val string_of_path : full_path -> string + val basename : full_path -> Names.Id.t type object_name = full_path * Names.KerName.t |