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 --- plugins/ssr/ssrparser.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssr/ssrparser.mli') 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 -- cgit v1.2.3