aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacenv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacenv.ml')
-rw-r--r--tactics/tacenv.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index d2d3f3117..cc87e197d 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -143,3 +143,5 @@ let register_ltac for_ml local id tac =
let redefine_ltac local kn tac =
Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
+
+let () = Hook.set Tactic_debug.is_ltac_for_ml_tactic_hook is_ltac_for_ml_tactic