From 479358ea0541b62ff33db1c18e898d99ae6826f2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2003 21:01:35 +0000
Subject: Réinstallation d'un afficheur de niveau d'imbrication pour le
 déboggueur de tactique

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

(limited to 'proofs/tactic_debug.mli')

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