test-suite/bugs/closed/5331.v


1
2
3
4
5
6
7
8
9
10
11

(* Checking no anomaly on some unexpected intropattern *)

Ltac ih H := induction H as H.
Ltac ih' H H' := induction H as H'.

Goal True -> True.
Fail intro H; ih H.
intro H; ih' H ipattern:([]).
exact I.
Qed.