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 /printing/prettyp.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 'printing/prettyp.mli')
-rw-r--r-- | printing/prettyp.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/prettyp.mli b/printing/prettyp.mli index dbd101159..31fd766ea 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -80,12 +80,12 @@ val print_located_module : reference -> Pp.t val print_located_other : string -> reference -> Pp.t type object_pr = { - print_inductive : mutual_inductive -> Pp.t; - print_constant_with_infos : constant -> Pp.t; + print_inductive : MutInd.t -> Pp.t; + print_constant_with_infos : Constant.t -> Pp.t; print_section_variable : variable -> Pp.t; - print_syntactic_def : kernel_name -> Pp.t; - print_module : bool -> Names.module_path -> Pp.t; - print_modtype : module_path -> Pp.t; + print_syntactic_def : KerName.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : Context.Named.Declaration.t -> Pp.t; print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; print_context : bool -> int option -> Lib.library_segment -> Pp.t; |