3993.v « closed « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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.