diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cb3a0aaed9..c4d8072ba5 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2039,7 +2039,7 @@ let _ = let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; @@ -2048,7 +2048,7 @@ let _ = optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } -let _ = +let () = let open Goptions in declare_bool_option { optdepr = false; |