From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Sun, 11 Jun 2017 15:14:15 +0200
Subject: deprecate Pp.std_ppcmds type alias

---
 plugins/ssr/ssrprinters.mli | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'plugins/ssr/ssrprinters.mli')

diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 5c68872b7..f23106826 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -11,16 +11,16 @@
 open Ssrast
 
 val pp_term :
-  Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds
+  Goal.goal Evd.sigma -> EConstr.constr -> Pp.t
 
-val pr_spc : unit -> Pp.std_ppcmds
-val pr_bar : unit -> Pp.std_ppcmds
+val pr_spc : unit -> Pp.t
+val pr_bar : unit -> Pp.t
 val pr_list : 
-  (unit -> Pp.std_ppcmds) -> ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
+  (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
 
 val pp_concat :
-  Pp.std_ppcmds ->
-  ?sep:Pp.std_ppcmds -> Pp.std_ppcmds list -> Pp.std_ppcmds
+  Pp.t ->
+  ?sep:Pp.t -> Pp.t list -> Pp.t
 
 val xInParens : ssrtermkind
 val xWithAt : ssrtermkind
@@ -29,17 +29,17 @@ val xCpattern : ssrtermkind
 
 val pr_term :
   ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
-  Pp.std_ppcmds
+  Pp.t
 
-val pr_hyp : ssrhyp -> Pp.std_ppcmds
+val pr_hyp : ssrhyp -> Pp.t
 
-val prl_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds
-val prl_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
+val prl_constr_expr : Constrexpr.constr_expr -> Pp.t
+val prl_glob_constr : Glob_term.glob_constr -> Pp.t
 
 val pr_guarded :
-  (string -> int -> bool) -> ('a -> Pp.std_ppcmds) -> 'a -> Pp.std_ppcmds
+  (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t
 
-val pr_occ : ssrocc -> Pp.std_ppcmds
+val pr_occ : ssrocc -> Pp.t
 
-val ppdebug : Pp.std_ppcmds Lazy.t -> unit
+val ppdebug : Pp.t Lazy.t -> unit
 
-- 
cgit v1.2.3