diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e6578ce52d..094cb6b19e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -491,6 +491,8 @@ END VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF | [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] +| [ "Clear" "Implicit" "Tactic" ] -> + [ Pfedit.clear_implicit_tactic () ] END |