From f086aed126f63d2db76be876d387beb8915d381a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 23 Jun 2015 19:24:22 +0200
Subject: Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.

---
 ltac/tacinterp.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 406fd41ad8..fcc29a8302 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -2172,4 +2172,14 @@ let _ =
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
 
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = false;
+      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