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

summary refs log tree commit diff

path: root/test-suite/bugs/closed/shouldsucceed/3000.v

blob: 27de34ed170f8da41d04982f1c12447bac61e733 (plain)

1 2	`Inductive t (t':Type) : Type := A \| B. Definition d := match t with _ => 1 end. (* used to fail on list_chop *)`