diff options
Diffstat (limited to 'tactics/tacenv.ml')
-rw-r--r-- | tactics/tacenv.ml | 2 |
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 |