The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Sun, Mar 15, 2009 at 05:05:17PM +0000, Edsko de Vries wrote:
> On Sun, Mar 15, 2009 at 05:43:25PM +0100, Thomas Braibant wrote:
> > Maybe I am wrong but it seems to be related to a bug we encountered,
> > where the n in induction n in your tactic is not linked to the
> > parameter integer(n) but to a "n" potentially appearing in the context
> > of your goal (and here, I expect you do not have such n in your
> > context).
> > 
> > If you write set (n:=1); my_induction 1664.  then your tactic works,
> > isn't it ?
> 
> Yes, indeed. Weird :)

Actually, I take that back. It doesn't. (See also reply to Samuel).

Edsko