coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent pattern matching?

From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
To: Randy Pollack <rpollack AT inf.ed.ac.uk>
Cc: Coq-Club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Dependent pattern matching?
Date: Wed, 10 Oct 2012 22:18:05 -0400

Hi,

On 10 oct. 2012, at 22:02, Randy Pollack
<rpollack AT inf.ed.ac.uk>
wrote:

<snip/>
> A related question: is Matthieu Sozeau's "Equations" supported in Coq
> 8.4? (All the files in the git repository are years old.)

Not for the 8.4 branch!

Cheers,
-- Matthieu

[Coq-Club] Dependent pattern matching?, Randy Pollack, 10/11/2012
- Re: [Coq-Club] Dependent pattern matching?, Matthieu Sozeau, 10/11/2012
- Re: [Coq-Club] Dependent pattern matching?, Benoit Montagu, 10/11/2012