diff options
| author | Hugo Herbelin | 2020-09-18 19:36:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-18 19:36:20 +0200 |
| commit | 5c08a3172bf7b10723b0d5d22e4cf998971482d7 (patch) | |
| tree | 02bdca5ad6fdd0d286cc7f12ba6370e1add47c13 /dev | |
| parent | 6b991f6111006cf4635b3321232d61c4f5c54f40 (diff) | |
| parent | 3466c08689439804e828f7b809e698346fa76a3b (diff) | |
Merge PR #12963: Formally deprecate the double induction tactic.
Reviewed-by: VincentSe
Ack-by: herbelin
Ack-by: olaure01
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions