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

---
 plugins/ltac/tacinterp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6a4bf577b..84049d4ed 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