From 9fc6e8201ea567a6b2c4ba115ce595791a67d336 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Jan 2003 18:45:37 +0000
Subject: Plus du tout de backtracking dans "Match term"; vrai Exit dans
 débogueur

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

(limited to 'proofs/tactic_debug.mli')

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