The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 7 oct. 08 à 13:42, Robin Green a écrit :

> Can anyone tell me what the apparently undocumented Equations  
> command is
> for, in the trunk version? It seems like it might be useful for my
> development.

Hi,

	this is a very experimental, proof of concept, unfinished piece of  
work by me, that
would maybe better live in another branch. Let's spoil it though: it's  
a primitive
implementation of a dependent pattern matching compiler (from  
equations to
Coq case-expressions, plus K when needed). IT DOES NOT WORK yet except  
for simple examples, but it will get properly documented when it does.

-- Matthieu