diff options
| author | Pierre-Marie Pédrot | 2020-09-01 12:18:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-17 08:07:59 +0200 |
| commit | 3466c08689439804e828f7b809e698346fa76a3b (patch) | |
| tree | 110a13095774ed47b2d8547831d724357299d468 /plugins/ltac | |
| parent | 3ff6af396ce73291a127707022aa2c96adc52b0b (diff) | |
Formally deprecate the double induction tactic.
The doc states it is deprecated since 1386cd9 but this was ages before the
deprecation mechanism existed.
Diffstat (limited to 'plugins/ltac')
| -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 |