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

---
 toplevel/vernacentries.ml | 17 ++++++++++++-----
 toplevel/vernacexpr.ml    |  3 +--
 2 files changed, 13 insertions(+), 7 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 033fb0e6..d384541f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 8751 2006-04-27 16:17:51Z courtieu $ i*)
+(*i $Id: vernacentries.ml 9017 2006-07-05 17:27:34Z herbelin $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -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 a00901a4..972d7ed9 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacexpr.ml 7936 2006-01-28 18:36:54Z herbelin $ i*)
+(*i $Id: vernacexpr.ml 9017 2006-07-05 17:27:34Z herbelin $ i*)
 
 open Util
 open Names
@@ -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
-- 
cgit v1.2.3