aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3993.v
blob: 086d8dd0f394667159e3ae5ed22d781cd4457ed9 (plain)
1
2
3
(* Test smooth failure on not fully applied term to destruct with eqn: given *)
Goal True.
Fail induction S eqn:H.