diff options
Diffstat (limited to 'plugins/ltac/tactic_debug.mli')
| -rw-r--r-- | plugins/ltac/tactic_debug.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 6cfaed3053..2475e41f9d 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Environ open Pattern open Names @@ -59,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 @@ -78,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 |