From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Thu, 13 Jul 2006 14:28:31 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta.2

---
 ide/coq.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 0b83b3c9..32e8a02e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 8912 2006-06-07 11:20:58Z notin $ *)
+(* $Id: coq.ml 9024 2006-07-06 10:38:15Z herbelin $ *)
 
 open Vernac
 open Vernacexpr
@@ -124,7 +124,7 @@ let interp verbosely s =
 	  | VernacDeclareTacticDefinition _
 		when is_in_proof_mode () -> 
 		  user_error_loc loc (str "CoqIDE do not support nested goals")
-	  | VernacDebug _ ->
+	  | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) ->
 	      user_error_loc loc (str "Debug mode not available within CoqIDE")
 	  | VernacResetName _
 	  | VernacResetInitial 
-- 
cgit v1.2.3