The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 18/06/2014 12:59, Beta Ziliani wrote:
> You have two options AFAIK: ask Ssreflect's devs to put the Canonical
> Instances in a module to import optionally, or to try some trick similar to
> the one we did in
> 
> http://www.mpi-sws.org/~beta/lessadhoc/
> 
> to deal with overlapping instances.
> 
> Right now I don't have the time to really look into your specific problem
> to help you out in a more direct way, but feel free to ask if you have any
> questions.

Yet, in Coq's code, the canonical structures are registered in a plain
table. I can't see any reason that would forbid removing things from
that table, thereby achieving what you're looking for... Maybe this
deserves a bug report to add such a new command?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature