3993.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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.