blob: 63e33b63f79f54ca1e7d21090374ff683a9cb382 (
plain)
1
2
3
4
5
|
(* Implicit arguments on type were missing for recursive records *)
Inductive foo {A : Type} : Type := { Foo : foo }.
(* Implicit arguments can be overidden *)
Inductive bar {A : Type} : Type := { Bar : @bar (A*A) }.
|
