From a4d496b2424ef991dfdd066e8138c321f62fd017 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Apr 2018 21:12:48 +0200
Subject: Making tactic-in-term aware of "Set Ltac Debug".

---
 CHANGES                   | 2 +-
 plugins/ltac/tacinterp.ml | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 234d6c0dbf..ed46150211 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,9 +14,9 @@ Vernacular Commands
 Tactic language
 
 - Support for fix/cofix added in Ltac "match" and "lazymatch".
-
 - Ltac backtraces now contain include trace information about tactics
   called by OCaml-defined tactics.
+- Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
 Changes from 8.8+beta1 to 8.8.0
 ===============================
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6a4bf577b1..84049d4ed5 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2010,7 +2010,8 @@ let interp_redexp env sigma r =
 
 let _ =
   let eval lfun env sigma ty tac =
-    let ist = { lfun = lfun; extra = TacStore.empty; } in
+    let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
+    let ist = { lfun = lfun; extra; } in
     let tac = interp_tactic ist tac in
     let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
     (EConstr.of_constr c, sigma)
-- 
cgit v1.2.3