The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Wed, Feb 24, 2010 at 12:39:19AM +0000, Ian Lynagh wrote:
> On Wed, Feb 24, 2010 at 12:54:43AM +0100, Adam Koprowski wrote:
> >
> > Below find my quick go at defining append in a more concise
> > way (starting with a replacement for your definition of Sequence).
> 
> Thanks! Unfortunately, it doesn't seem to work for me. Here:
> 
> > Inductive Sequence : forall (from to : NameSet.t) (contains : ThingSet.t),
> > Type :=
> >   | Nil : forall `{t : NameSet.t, e [=] ThingSet.empty}, t --[e]-> t
> >   | Cons : forall `{p : Patch from mid, s : Sequence mid to contains, e 
> > [=]
> > (ThingSet.add (thingOf p) contains)}, from --[e]-> to
> > where "s --[ c ]-> t ":= (Sequence s t c).
> 
> I get:
>     Error: Unbound and ungeneralizable variable e
> on the first occurence of e (before the [=], on the Nil line).
> 
> Any idea what's wrong? I have trunk 12801.

mattam has just told me on IRC that the answer is that:
    Generalizable All Variables.
is now needed.


Thanks
Ian