From 40c483a95f354e457e10d00951fd6a8eec08176d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 5 Nov 2018 13:32:36 -0800
Subject: Document undocumented flags and options Also remove a few
 undocumented settings

---
 plugins/ltac/tacinterp.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index c4d8072ba5..cf5eb442be 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2048,13 +2048,4 @@ let () =
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
 
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "Ltac debug";
-      optkey   = ["Debug";"Ltac"];
-      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
-      optwrite = vernac_debug }
-
 let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
-- 
cgit v1.2.3