aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/4624.v
blob: a737afcdabe116cfa3affeecbcc44a296daaae8b (plain)
1
2
3
4
5
6
7
Record foo := mkfoo { type : Type }.

Canonical Structure fooA (T : Type) := mkfoo (T -> T).

Definition id (t : foo) (x : type t) := x.

Definition bar := id _ ((fun x : nat => x) : _).