aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-04 18:58:27 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:05:31 +0100
commitf3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch)
treefceac407f6e4254e107817b6140257bcc8f9755a /printing/prettyp.mli
parent0d81e80a09db7d352408be4dfc5ba263f6ed98ef (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.mli10
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;