aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tactic_debug.mli
diff options
context:
space:
mode:
authorMatej Košík2017-06-11 15:14:15 +0200
committerMatej Košík2017-07-27 10:10:23 +0200
commite3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch)
treea9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /plugins/ltac/tactic_debug.mli
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'plugins/ltac/tactic_debug.mli')
-rw-r--r--plugins/ltac/tactic_debug.mli8
1 files changed, 4 insertions, 4 deletions
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