aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2303.v
blob: e614b9b55281d8d5545889baa6b0713f6957a125 (plain)
1
2
3
4
Class A := a: unit.
Class B (x: unit).
Axiom H: forall x: A, @B x -> x = x -> unit.
Definition Field (z: A) (m: @B z) x := (@H _ _ x) = z.