diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/coretactics.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index cb226de586..f1f538ab39 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -263,7 +263,7 @@ END (** Double induction *) -TACTIC EXTEND double_induction +TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () } | [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> { Elim.h_double_induction h1 h2 } END |