On 2010-01-14 12:38, Florent Balestrieri wrote: > In lib-0.3, is there a reason why all equivalence relations which are > record parameters in the module Algebra.Structure are constrained to be > in Set 0 ? Yes: no one has generalised the code yet. -- /NAD