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

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