The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have a goal where "rewrite @foo by auto with typeclass_instances." fails with "Unable to find an instance for the variables H, H0.", but "erewrite @foo by auto with typeclass_instances." succeeds and doesn't leave over typeclass goals (that is, [Show Existentials.] shows only the goal as an existential instance, not other typeclass goals).  I thought typeclass hints were supposed to automatically trigger and be resolved.  Can someone explain to me what's happening here, and possibly how to fix it so I can add [@foo] to a hint database to be used with [autorewrite]?

I'll send a minimal example to the list soon, if no one answers before I get around to making one.

Thanks,

Jason