The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

I was planning to formalize meson procedure as described in john
harrison´s forthcoming book. The idea was to be as close as possible
to his code. I got distracted by other things, but I do have the
unification.

The code is available at

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/unif.tar.gz

compared to Rouyer work, the term structure is more natural.


--
Laurent Théry