The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

https://coq.inria.fr/bugs/show_bug.cgi?id=3841 , https://coq.inria.fr/bugs/show_bug.cgi?id=3495 

On Wed, Jul 27, 2016 at 8:24 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 07/27/2016 11:14 AM, Jason Gross wrote:
> Have you tried using Tactic Notation and ident, if I recall correctly?
> There should be a way to interpret a symbol as a name rather than as a
> constr.

There should be, but I can't find it.  I tried ident and uconstr and
reference and simple_intropattern, but it seems like @silly is distinct
from silly in a way that nothing can convert between.

>
> I think that the extra typeclass resolution is related to a bug I ran into
> in 8.4 a while back, where if you have an implicit argument which is an
> unresolable typeclass, and the argument doesn't appear in the type, and you
> [eapply] the lemma, then just about every subsequent tactic (reflexivity,
> destruct, etc, but not refine) will fail with a typeclass resolution error.

Sounds horrible.  Do you have an example of that?  Or the bugzilla
number for it?

-- Jonathan