diff options
Diffstat (limited to 'proofs/tactic_debug.mli')
| -rw-r--r-- | proofs/tactic_debug.mli | 40 |
1 files changed, 19 insertions, 21 deletions
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index b4c05324..e4c0a23e 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,22 +8,20 @@ open Environ open Pattern -open Evd -open Proof_type open Names open Tacexpr open Term +open Evd (** This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework *) -val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit -val set_match_pattern_printer : - (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit -val set_match_rule_printer : - ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> - unit +val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t +val match_pattern_printer : + (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t +val match_rule_printer : + ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t (** Debug information *) type debug_info = @@ -32,37 +30,37 @@ type debug_info = (** Prints the state and waits *) val debug_prompt : - int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a + int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic (** Initializes debugger *) -val db_initialize : unit -> unit +val db_initialize : unit Proofview.NonLogical.t (** Prints a constr *) -val db_constr : debug_info -> env -> constr -> unit +val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit + debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t (** Prints a matched hypothesis *) val db_matched_hyp : - debug_info -> env -> identifier * constr option * constr -> name -> unit + debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t (** Prints the matched conclusion *) -val db_matched_concl : debug_info -> env -> constr -> unit +val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t (** Prints a success message when the goal has been matched *) -val db_mc_pattern_success : debug_info -> unit +val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t (** Prints a failure message for an hypothesis pattern *) val db_hyp_pattern_failure : - debug_info -> env -> name * constr_pattern match_pattern -> unit + debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t (** Prints a matching failure message for a rule *) -val db_matching_failure : debug_info -> unit +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 +val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t (** An exception handler *) val explain_logic_error: (exn -> Pp.std_ppcmds) ref @@ -74,8 +72,8 @@ val explain_logic_error: (exn -> Pp.std_ppcmds) ref val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref (** Prints a logic failure message for a rule *) -val db_logic_failure : debug_info -> exn -> unit +val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - identifier Util.located message_token list -> unit + Id.t Loc.located message_token list -> unit Proofview.NonLogical.t |