diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-05 17:27:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-05 17:27:34 +0000 |
| commit | 6e38fa3afac77cea982cf4967e7fa9808e6fc7fa (patch) | |
| tree | ec7d8428a65ad0cf725accd46a2a14eb9c378106 /toplevel | |
| parent | ec2a4b3402e901067a4295996028decbd9f6671f (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 15 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
2 files changed, 11 insertions, 5 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 42f7ec71b..5c0ac05f0 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 0ba2610c4..51010afa8 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 |