diff options
author | Matej Košík <matej.kosik@inria.fr> | 2017-06-11 15:14:15 +0200 |
---|---|---|
committer | Matej Košík <matej.kosik@inria.fr> | 2017-07-27 10:10:23 +0200 |
commit | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch) | |
tree | a9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /plugins/ssr | |
parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) |
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'plugins/ssr')
-rw-r--r-- | plugins/ssr/ssrcommon.mli | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.mli | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrprinters.mli | 26 |
3 files changed, 15 insertions, 15 deletions
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 |