Debugger plus informatif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 34 insertions, 6 deletions

diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 9b542c7848..8c5dc9d03c 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -8,8 +8,11 @@
 
 (*i $Id$ i*)
 
+open Environ
+open Pattern
 open Proof_type
 open Names
+open Tacexpr
 open Term
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -18,18 +21,43 @@ open Term
 
 (* Debug information *)
 type debug_info =
-  | DebugOn of int
+  | DebugOn
   | DebugOff
+  | Run of int
 
 (* Prints the state and waits *)
-val debug_prompt : int -> goal sigma option -> Tacexpr.raw_tactic_expr ->
-      (debug_info -> 'a) -> 'a
+val debug_prompt :
+  goal sigma -> debug_info -> Tacexpr.raw_tactic_expr -> debug_info
 
 (* Prints a constr *)
-val db_constr : debug_info -> Environ.env -> constr -> unit
+val db_constr : debug_info -> env -> constr -> unit
+
+(* Prints the pattern rule *)
+val db_pattern_rule :
+  debug_info -> int -> (pattern_expr,raw_tactic_expr) match_rule -> unit
 
 (* Prints a matched hypothesis *)
-val db_matched_hyp : debug_info -> Environ.env -> identifier * constr -> unit
+val db_matched_hyp :
+  debug_info -> env -> identifier * constr -> identifier option -> unit
 
 (* Prints the matched conclusion *)
-val db_matched_concl : debug_info -> Environ.env -> constr -> unit
+val db_matched_concl : debug_info -> env -> constr -> unit
+
+(* Prints a success message when the goal has been matched *)
+val db_mc_pattern_success : debug_info -> unit
+
+(* Prints a failure message for an hypothesis pattern *)
+val db_hyp_pattern_failure :
+  debug_info -> env -> identifier option * constr_pattern match_pattern -> unit
+
+(* Prints a matching failure message for a rule *)
+val db_matching_failure : debug_info -> unit
+
+(* Prints an evaluation failure message for a rule *)
+val db_eval_failure : debug_info -> unit
+
+(* An exception handler *)
+val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+
+(* Prints a logic failure message for a rule *)
+val db_logic_failure : debug_info -> exn -> unit