coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] apply, auto, and implicit type classes

From: Tom Prince <tom.prince AT ualberta.net>
To: Aaron Bohannon <bohannon AT cis.upenn.edu>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] apply, auto, and implicit type classes
Date: Mon, 14 Feb 2011 21:20:39 -0500

On 2011-02-15, Aaron Bohannon wrote:
> Hi,
>
> I have found a strange behavior.  Consider this custom tactic:
>
> Tactic Notation "foo" constr(e) constr(e1) :=
>   apply e with (1 := e1).
>
> I have a proof state in which "apply lemma with (1 := H)" succeeds as
> expected; however "foo lemma H" fails.

I don't know whether this behaviour is expected, but the typeclass
mechanism still has kinks and oddities in it. It would probably help if
you gave a small self contained example of this behavior (and the
behviour of auto) occurring.

  Tom.

[Coq-Club] apply, auto, and implicit type classes, Aaron Bohannon
- Re: [Coq-Club] apply, auto, and implicit type classes, Tom Prince
  - Re: [Coq-Club] apply, auto, and implicit type classes, Aaron Bohannon
    - Re: [Coq-Club] apply, auto, and implicit type classes, Tom Prince