diff options
Diffstat (limited to 'tactics/tacenv.ml')
| -rw-r--r-- | tactics/tacenv.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index cc87e197d1..d2d3f3117f 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -143,5 +143,3 @@ 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 |