From fbe1a5c31a962a8e20199986a914f1db7991170c Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:36:10 +0000 Subject: Makes the Ltac debugger usable again. This is just a port of the existing design. Basing the tactics on an IO monad may allow to simplify things a bit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16985 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/tactic_debug.mli | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'proofs/tactic_debug.mli') 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 -- cgit v1.2.3