[Agda] error in plfa exercise

[Michel Levy]

When I try to reproduce the currying proof, I get the following error
Expected non-abstract record type, found
(.A → .B → .C) ≃ .A x .B → .C
when checking that the expression
record
{ to = λ { f → λ { < x , y > → (f x) y } }
from = λ { g → λ { x y → g < x , y > } }
; from∘to = λ { f → refl }
; to∘from = λ { g → extensionality λ { < x , y > → refl } }
}
has type (.A → .B → .C) ≃ .A x .B → .C

Where does this error come from, from my too old version of agda?

-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr