From 6e38fa3afac77cea982cf4967e7fa9808e6fc7fa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 5 Jul 2006 17:27:34 +0000
Subject: Branchement de 'Debug On/Off' sur le mécanisme standard d'option et
 donc, renommage en 'Set/Unset Ltac Debug' en prévision documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9017 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 68ef987498..737c97bae3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -652,8 +652,11 @@ GEXTEND Gram
 	  VernacBacktrack (n,m,p)
 
 (* Tactic Debugger *)
-      |	IDENT "Debug"; IDENT "On" -> VernacDebug true
-      |	IDENT "Debug"; IDENT "Off" -> VernacDebug false
+      |	IDENT "Debug"; IDENT "On" -> 
+          VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue true)
+
+      |	IDENT "Debug"; IDENT "Off" ->
+          VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue false)
 
  ] ];
     END
-- 
cgit v1.2.3