The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

If you have a better behaviour to suggest for `coqchk` please do. But I'm not sure it will be easy, unfortunately.

On 29 March 2015 at 19:54, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/29/2015 01:41 PM, Enrico Tassi wrote:

On Sun, Mar 29, 2015 at 01:27:25PM -0400, Jonathan Leivent wrote:

Even worse - a file that just says:

  Require Import EquivDec.

when run through coqchk -o will produce:

Coqchk prints all the axioms, as in "Axiom" keyword, loaded in the
environment.  "Print Assumptions name" prints only the ones used by
name.

Best,

Right - I should have inferred that.  Although that coqchk -o behavior seems not too useful, in that case.

-- Jonathan