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

3 files changed, 16 insertions, 7 deletions

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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 42f7ec71b8..5c0ac05f0c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -789,6 +789,17 @@ let _ =
       optread=Pp_control.get_margin;
       optwrite=Pp_control.set_margin }
 
+let vernac_debug b =
+  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
+
+let _ =
+  declare_bool_option
+    { optsync=false;
+      optkey=SecondaryTable("Ltac","Debug");
+      optname="Ltac debug";
+      optread=(fun () -> get_debug () <> Tactic_debug.DebugOff);
+      optwrite=vernac_debug }
+
 let vernac_set_opacity opaq locqid =
   match Nametab.global locqid with
     | ConstRef sp ->
@@ -1069,9 +1080,6 @@ let vernac_check_guard () =
   in 
   msgnl message
 
-let vernac_debug b =
-  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
-
 let interp c = match c with
   (* Control (done in vernac) *)
   | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false
@@ -1175,7 +1183,6 @@ let interp c = match c with
   | VernacGo g -> vernac_go g
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacDebug b -> vernac_debug b
   | VernacProof tac -> vernac_set_end_tac tac
   (* Toplevel control *)
   | VernacToplevelControl e -> raise e
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 0ba2610c4b..51010afa80 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -281,7 +281,6 @@ type vernac_expr =
   | VernacGo of goable
   | VernacShow of showable
   | VernacCheckGuard
-  | VernacDebug of bool
   | VernacProof of raw_tactic_expr
   (* Toplevel control *)
   | VernacToplevelControl of exn