diff options
| author | Pierre-Marie Pédrot | 2016-03-06 21:25:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 21:28:09 +0100 |
| commit | cdc91f02f98b4d857bfebe61d95b920787a8d0e5 (patch) | |
| tree | eefe365468ee275445ce0a00395d602f7c1ab48f /tactics/tactic_debug.ml | |
| parent | 6f49db55e525a57378ca5600476c870a98a59dae (diff) | |
Putting Tactic_debug just below Tacinterp.
Diffstat (limited to 'tactics/tactic_debug.ml')
| -rw-r--r-- | tactics/tactic_debug.ml | 6 |
1 files changed, 2 insertions, 4 deletions
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 |