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 /library/libnames.mli | |
| 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 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index ab2585334..ed01163ee 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -11,12 +11,13 @@ open Loc open Names (** {6 Dirpaths } *) -(** FIXME: ought to be in Names.dir_path *) +val dirpath_of_string : string -> DirPath.t val pr_dirpath : DirPath.t -> Pp.t +[@@ocaml.deprecated "Alias for DirPath.print"] -val dirpath_of_string : string -> DirPath.t val string_of_dirpath : DirPath.t -> string +[@@ocaml.deprecated "Alias for DirPath.to_string"] (** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *) val pop_dirpath : DirPath.t -> DirPath.t @@ -127,7 +128,20 @@ val pr_reference : reference -> Pp.t val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference -(** Deprecated synonyms *) +(** some preset paths *) +val default_library : DirPath.t + +(** This is the root of the standard library of Coq *) +val coq_root : module_ident (** "Coq" *) +val coq_string : string (** "Coq" *) +(** This is the default root prefix for developments which doesn't + mention a root *) +val default_root_prefix : DirPath.t + +(** Deprecated synonyms *) val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *) +[@@ocaml.deprecated "Alias for qualid_of_ident"] + val qualid_of_sp : full_path -> qualid (** = qualid_of_path *) +[@@ocaml.deprecated "Alias for qualid_of_sp"] |