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/ltac/tactic_debug.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/tactic_debug.mli')

diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index ef6362270a..2475e41f9d 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -58,16 +58,16 @@ val db_hyp_pattern_failure :
 val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
 
 (** Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
+val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t
 
 (** An exception handler *)
-val explain_logic_error: exn -> Pp.std_ppcmds
+val explain_logic_error: exn -> Pp.t
 
 (** For use in the Ltac debugger: some exception that are usually
    consider anomalies are acceptable because they are caught later in
    the process that is being debugged.  One should not require
    from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds
+val explain_logic_error_no_anomaly : exn -> Pp.t
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
@@ -77,4 +77,4 @@ val db_breakpoint : debug_info ->
   Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
-  ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located
+  ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
-- 
cgit v1.2.3