coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Mon, 22 Aug 2016 06:33:36 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f177.google.com
Ironport-phdr: 9a23:1X1tLx3lCDBbUxQqsmDT+DRfVm0co7zxezQtwd8ZsegQLPad9pjvdHbS+e9qxAeQG96KsrQf06GG7eigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV4Qz2rjKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduYCgJ45jgsgCGRg+S7DNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPFs3sTKt8dT2n9O8/Qx/yiTxBOzc86yfRjuR/iatapFSqoBkpkN2cW52cKPcrJvCVRtgdX2cUBss=

Dear All,

When reading this conversation I got the idea that there could be a "Require Import NoAxiom Module." that imports only the parts of a library that are not axioms and also do not depend on axioms. If one does this, coqchk could also just take this into account and not report the axioms in the library.

Regards,

Chris

Re: [Coq-Club] Axioms reported by coqchk, (continued)
- Re: [Coq-Club] Axioms reported by coqchk, Ade Umut Huxtable, 08/21/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/22/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ade Umut Huxtable, 08/22/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Chris Dams, 08/22/2016