From 4767404bdc47e8148ab5ea171a0abb43795b01cf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Jan 2003 21:53:07 +0000
Subject: Restructuration interpréteur de tactique: plus d'évaluation partielle
 à la définition; suppression TacFunRec, VClosure, VFTactic et VContext;
 davantage de globalisation statique (notamment pour les tactiques
 mutuellement récursives); débogueur plus informatif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3529 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tactic_debug.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs/tactic_debug.mli')

diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index b05a33fdfc..1bb8a7f42d 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -18,12 +18,13 @@ open Term
 
 (* Debug information *)
 type debug_info =
-  | DebugOn
+  | DebugOn of int
   | DebugOff
   | Exit
 
 (* Prints the state and waits *)
-val debug_prompt : goal sigma option -> Tacexpr.raw_tactic_expr -> debug_info
+val debug_prompt : int -> goal sigma option -> Tacexpr.raw_tactic_expr ->
+      (debug_info -> 'a) -> (unit -> 'a) -> 'a
 
 (* Prints a constr *)
 val db_constr : debug_info -> Environ.env -> constr -> unit
-- 
cgit v1.2.3