On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:

> Yet, modules are strange beasts for typing, so I wouldn't add the code
> before thinking it through.

I am curious as to the status of COQ support for verifying
assertions about proposed changes to the type system.

For example supposing you did 'think it through' and it
seemed right, would you be able to then extend an
existing COQ proof and attempt to prove your thinking
mechanically?

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net