2231.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/2231.v

blob: 03e2c9bbf41a4424beb33dea6e34b3ed6e8029e5 (plain)

1
2
3

Inductive unit2 : Type := U : unit -> unit2.
Inductive dummy (u: unit2) : unit -> Type :=
          V: dummy u (let (tt) := u in tt).