From cdc91f02f98b4d857bfebe61d95b920787a8d0e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 21:25:20 +0100
Subject: Putting Tactic_debug just below Tacinterp.

---
 tactics/tactic_debug.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'tactics/tactic_debug.ml')

diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml
index fa40b74160..e991eb86dc 100644
--- a/tactics/tactic_debug.ml
+++ b/tactics/tactic_debug.ml
@@ -325,12 +325,10 @@ let db_breakpoint debug s =
 
 (** Extrating traces *)
 
-let (is_for_ml_f, is_ltac_for_ml_tactic_hook) = Hook.make ()
-
 let is_defined_ltac trace =
   let rec aux = function
   | (_, Tacexpr.LtacNameCall f) :: tail ->
-      not (Hook.get is_for_ml_f f)
+      not (Tacenv.is_ltac_for_ml_tactic f)
   | (_, Tacexpr.LtacAtomCall _) :: tail ->
       false
   | _ :: tail -> aux tail
@@ -373,7 +371,7 @@ let explain_ltac_call_trace last trace loc =
 let skip_extensions trace =
   let rec aux = function
   | (_,Tacexpr.LtacNameCall f as tac) :: _ 
-      when Hook.get is_for_ml_f f -> [tac]
+      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
   | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
       :: _ -> [tac]
   | t :: tail -> t :: aux tail
-- 
cgit v1.2.3