The Coq mailing list

[Samuel Bronson <naesten AT gmail.com>]

Pierre Letouzey <Pierre.Letouzey <at> pps.jussieu.fr> writes:

> and impossible, due to the new features of the soon-to-be-called 8.2
> in terms of modules, rewrite, and other new cool features.

I think you forgot to mention type classes? They seem to be central to the
workings of the new setoid support. I base this fact that it allowed me to use
setoid rewritings in no particular setoid -- that is, the setoid was a 
typeclass
constraint on the type of the definition I was building.