diff options
Diffstat (limited to 'proofs/tactic_debug.mli')
| -rw-r--r-- | proofs/tactic_debug.mli | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 3b9858f16..1ae1a3905 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -31,37 +31,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 -> (Tacexpr.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 -> Id.t * constr option * constr -> Name.t -> 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.t * constr_pattern match_pattern -> unit + debug_info -> env -> 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 @@ -73,8 +73,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 -> - Id.t Loc.located message_token list -> unit + Id.t Loc.located message_token list -> unit Proofview.NonLogical.t |