diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /library/nametab.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'library/nametab.mli')
| -rw-r--r-- | library/nametab.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 3a380637c..c02447a7c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -74,7 +74,7 @@ val error_global_not_found : ?loc:Loc.t -> qualid -> 'a type visibility = Until of int | Exactly of int val push : visibility -> full_path -> global_reference -> unit -val push_modtype : visibility -> full_path -> module_path -> unit +val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit @@ -85,11 +85,11 @@ val push_syndef : visibility -> full_path -> syndef_name -> unit val locate : qualid -> global_reference val locate_extended : qualid -> extended_global_reference -val locate_constant : qualid -> constant +val locate_constant : qualid -> Constant.t val locate_syndef : qualid -> syndef_name -val locate_modtype : qualid -> module_path +val locate_modtype : qualid -> ModPath.t val locate_dir : qualid -> global_dir_reference -val locate_module : qualid -> module_path +val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t (** These functions globalize user-level references into global @@ -105,7 +105,7 @@ val global_inductive : reference -> inductive val locate_all : qualid -> global_reference list val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_dir : qualid -> global_dir_reference list -val locate_extended_all_modtype : qualid -> module_path list +val locate_extended_all_modtype : qualid -> ModPath.t list (** Mapping a full path to a global reference *) @@ -135,8 +135,8 @@ val full_name_module : qualid -> DirPath.t val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path -val dirpath_of_module : module_path -> DirPath.t -val path_of_modtype : module_path -> full_path +val dirpath_of_module : ModPath.t -> DirPath.t +val path_of_modtype : ModPath.t -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) @@ -156,8 +156,8 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid -val shortest_qualid_of_modtype : module_path -> qualid -val shortest_qualid_of_module : module_path -> qualid +val shortest_qualid_of_modtype : ModPath.t -> qualid +val shortest_qualid_of_module : ModPath.t -> qualid (** Deprecated synonyms *) |