The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Op dinsdag 25-05-2010 om 12:52 uur [tijdzone +0100], schreef Martijn
Vermaat:
> I stumbled upon a strange (to me) problem with dependent destruction
> (or
> dependent induction for that matter) where it gets stuck in a cycle. 

I could add that I use the 8.3-beta0-1 version of Coq or current SVN,
both do the same thing here.

Trying Coq 8.2pl1, dependent destruction fails in the destruct
invocation saying that it would lead to a term that is ill-typed.

I am not so much interested in Coq 8.2 at this point, since there are
still some other parts of the development that I cannot get to work in
it. I focus on 8.3 which is mostly working for me.

kind regards,
Martijn