coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq pattern matching going crazy on me -> looks like a bug.

From: Chris Dams <chris.dams.nl AT gmail.com>
To: Chris Dams <chris.dams.nl AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq pattern matching going crazy on me -> looks like a bug.
Date: Wed, 17 Feb 2010 15:27:24 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=TA84L1HEt8pftxfJQ42vcuvzRlBjSJUDiXIIK9b6ChcuTRahdiVZp9GCi684W293ne JPKIK3r1pwZ16aL39rBsF5X4BCb7TSTnnNcLZ0AA+oXi/yTLjkIK3bGsrBejGDaP+wKm VSaP/jAnbcEDyHrPQRUbEqi5t2PRQndZgqBz0=

Hello Hugo, Adam and others,

2010/2/14 Hugo Herbelin
<Hugo.Herbelin AT inria.fr>:

> The development versions behave well but unfortunately not the
> 8.2pl1.

Okay, thanks, I now compiled the trunk and that works fine! Cool.

> Sorry.

Well, you already brought us the otherwise great Coq program, so I forgive
you.

@Adam: yes, probably it can be done more easily, but the code that I
posted was hugely simplified from what I am actually working that, so
that is not so very relevant for me. Actually, I found out about the
problem because the inversion tactic was failing mysteriously and by
trying to construct by hand the proof term that the inversion tactic
would have constructed.

All the best,
Chris

[Coq-Club] Coq pattern matching going crazy on me -> looks like a bug., Chris Dams
- Re: [Coq-Club] Coq pattern matching going crazy on me -> looks like a bug., Adam Chlipala
- Re: [Coq-Club] Coq pattern matching going crazy on me -> looks like a bug., Hugo Herbelin
  - Re: [Coq-Club] Coq pattern matching going crazy on me -> looks like a bug., Chris Dams