The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

> I would argue that this is a question of a slightly more general policy:
>  Should libraries strive to provide as much functionality as possible 
> without
> importing any axioms?  Not just "Program" is affected here, but also, e.g.,
> Psatz and Eqdep_dec (the latter importing

my opinion is that axioms should be in separate modules which have the word 
"Axiom" in their name and that these modules should not be imported by other 
library modules (without Axiom in their name). If one needs a module which 
requires certain axioms, then I would prefer to first explicitly import the 
axiom module and then the dependent module. What would help here is a 
mechanism with which a module can state that it requires a module, without 
actually importing it. Something like:

Require Check AxiomXYZ

If the module AxiomXYZ is not already imported, this should result in an 
error and otherwise do nothing.

Everybody is free to bundle the axioms and modules he needs in a way 
convenient for his work. This is much easier than finding out what innocent 
looking library modules require what axioms after the facts.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928