The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

It should be a feature report, not a bug report, I think!

On Wed, Jun 18, 2014 at 2:48 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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