The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

> I'm not so much a fan of Existing Class as a standard way to get this done,
> mostly because it is not a controllable declaration (there is no Local 
> variant,
> and it greedily makes instances out of all subsequent matching declarations
> (but not definitions!).). Having an alternative definition of UIP_dec that
> expects an actual typeclass instance instead would be better, if all of the
> individual eqdec definitions were instances.

I will test the variant with a dedicated decidable equality typeclass and a 
UIP_dec variant taking an instance of it and see how smooth it works. If I am 
happy with it, I will make a pull request on an extension of the library.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928