coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type checking in apply-with-in

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: Petar Maksimovic <petar.maksimovic AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Type checking in apply-with-in
Date: Thu, 23 Jan 2014 20:01:30 +0100

On 23/01/2014 14:53, Petar Maksimovic wrote:
> Is this a bug, a feature, something else?

Sounds like a bug.

Handling of with clauses in apply-related tactics is quite rustic, as
(for the Coq gurus of you) it relies on metas rather than evars. Thus
it's no surprise that you're able to do gory things with it. I even
think I have seen some similar bug to yours on the bugtracker.

I'm reporting it anyway, thanks.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Type checking in apply-with-in, Petar Maksimovic, 01/23/2014
- Re: [Coq-Club] Type checking in apply-with-in, Pierre-Marie Pédrot, 01/23/2014
  - Re: [Coq-Club] Type checking in apply-with-in, Pierre-Marie Pédrot, 01/23/2014
    - Re: [Coq-Club] Type checking in apply-with-in, Petar Maksimovic, 01/23/2014