test-suite/bugs/closed/5286.v


1
2
3
4
5
6
7
8
9

Set Primitive Projections.

CoInductive R := mkR { p : unit }.

CoFixpoint foo := mkR tt.

Check (eq_refl tt : p foo = tt).
Check (eq_refl tt <: p foo = tt).
Check (eq_refl tt <<: p foo = tt).