The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Mon, 1 Aug 2011 20:08:22 +0200
Stéphane Lescuyer 
<stephane.lescuyer AT polytechnique.org>
 wrote:

> For what it's worth, there's an approach that gives you the best of both 
> worlds...

Interesting!

This does shed new light on a few things. I expect I'll rewrite the
existing formalization to take advantage.