diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 19:01:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 19:36:03 +0100 |
| commit | 9e96794d6a4327761ce1ff992351199919431be1 (patch) | |
| tree | 389b2b091c2d186490943c6db92c5eaa452bb5f4 /toplevel/vernacentries.ml | |
| parent | 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (diff) | |
Moving Tactic_debug to tactics/ folder.
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 38832b422..d769c6033 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1433,18 +1433,6 @@ let _ = optread = Flags.get_dump_bytecode; optwrite = Flags.set_dump_bytecode } -let vernac_debug b = - set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) - -let _ = - declare_bool_option - { optsync = false; - optdepr = false; - optname = "Ltac debug"; - optkey = ["Ltac";"Debug"]; - optread = (fun () -> get_debug () != Tactic_debug.DebugOff); - optwrite = vernac_debug } - let _ = declare_bool_option { optsync = true; |