The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/09/2016 09:06 PM, Jason Gross wrote:
> > But, is there a way to have something print both foo_a and foo_b?
> Axiom A : Type.
> Existing Class A.
> Axioms a a' : A.
> Existing Instances a a'.
>
> Class MultiA {x : A} := dummy : True.
>
> Hint Extern 0 (@MultiA ?x) => idtac x; fail : typeclass_instances.
>
> Goal True.
>    try pose (_ : MultiA).
> (* a'
> a
> a'
> a
> a'
> a
> a'
> a *)
>
>
> Not sure why there's so much duplication, but can you make this work?

That's a strange solution.  But, as far as I can tell, it can only 
print.  One can't make other use of the non-most-recent instances, 
right?  In fact, MultiA has to not have any actual instances for this to 
work, it seems.

-- Jonathan