coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply without TC inference

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Apply without TC inference
Date: Wed, 27 Jul 2016 11:24:10 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
Ironport-phdr: 9a23:shkXAx/UnzkJBv9uRHKM819IXTAuvvDOBiVQ1KB90OkcTK2v8tzYMVDF4r011RmSDN2dta8P27OempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EkfqKrR8WC1oye7KObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrpT4wJk2+CNJ/vkl6sRoUKPgfq1+Q6YLIi4hNjUX48viqRnKS0Or63oCX2MK2k5KBA7E7xz+U5rZvS7zt+470y6fa56lBYsoUCivuv84ACTjjz0KYmY0

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

[Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
  - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
    - Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
      - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
    - Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
  - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
    - Re: [Coq-Club] Apply without TC inference, Matthieu Sozeau, 07/27/2016
      - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Clément Pit--Claudel, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016