test-suite/output/Projections.v


1
2
3
4
5
6
7
8
9
10
11


Set Printing Projections.

Class HostFunction := host_func : Type.

Section store.
  Context `{HostFunction}.
  Record store := { store_funcs : host_func }.
End store.

Check (fun (S:@store nat) => S.(store_funcs)).