The Coq mailing list

[Victor Porton <porton AT narod.ru>]

[Oh, sorry, I previously sent this email to a wrong mailing list.]

I suggest to add the following feature to Coq:

Make a modified "Import" statement (possible syntax: "Import Safe 
MODULENAME.").

This would transform every axiom (or parameter) in the imported module into a 
theorem condition, just like as it is done with sections.

This is especially useful for researching interrelations of several different 
axiom systems.

--
Victor Porton - http://portonvictor.org