Hi Freek, Freek Wiedijk <freek@cs.ru.nl> writes: > In the case of Georges Gonthier's language (which I do indeed > like very much), you're kind of right. But really it's _not_ > well integrated into Coq-as-a-system, I think. It's really a > layer on top of it. What is Georges Gonthier's language? Jesse -- Jesse Alama (alama@stanford.edu)