From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Sun, 11 Jun 2017 15:14:15 +0200 Subject: deprecate Pp.std_ppcmds type alias --- library/keys.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/keys.mli') diff --git a/library/keys.mli b/library/keys.mli index 6fe9efc6e..d5dc0e2a1 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -19,5 +19,5 @@ val equiv_keys : key -> key -> bool val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) -val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds +val pr_keys : (global_reference -> Pp.t) -> Pp.t (** Pretty-print the mapping *) -- cgit v1.2.3