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/ssrcommon.mli   |  2 +-
 plugins/ssr/ssrparser.mli   |  2 +-
 plugins/ssr/ssrprinters.mli | 26 +++++++++++++-------------
 3 files changed, 15 insertions(+), 15 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 4b045e989..2eadd5f26 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -41,7 +41,7 @@ val nohint : 'a ssrhint
 
 (******************************** misc ************************************)
 
-val errorstrm : Pp.std_ppcmds -> 'a
+val errorstrm : Pp.t -> 'a
 val anomaly : string -> 'a
 
 val array_app_tl : 'a array -> 'a list -> 'a list
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index bf6f44f11..88beeaa71 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -16,5 +16,5 @@ val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
 
-val add_genarg : string -> ('a -> Pp.std_ppcmds) -> 'a Genarg.uniform_genarg_type
+val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
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