From 2269d0844f8f8bc25bb2517cc90e02ad5c0e67bc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Jul 2006 10:38:15 +0000
Subject: Remplacement VernacDebug par VernacSetOption (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9024 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/coq.ml b/ide/coq.ml
index 62175aee81..37511f5a75 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -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