The Coq mailing list

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

Dear Jonathan,

> To be clear - are people suggesting that if axioms in the standard 
> libraries are
> placed in separate modules, then they don't believe a tool that can check 
> the
> actual dependency of a development on axioms is desirable?

a good tool for checking axiom dependencies is of cause desirable.

But nevertheless it should be an exception to drag in axioms. With the 
standard library as is, it can be tricky to avoid certain axioms and it is 
not likely that the result of the first axiom check on a development is 
without surprises.

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