coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] difference between coqchk and Print Assumptions

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] difference between coqchk and Print Assumptions
Date: Sun, 29 Mar 2015 13:54:50 -0400

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

[Coq-Club] difference between coqchk and Print Assumptions, Jonathan Leivent, 03/29/2015
- Re: [Coq-Club] difference between coqchk and Print Assumptions, Jonathan Leivent, 03/29/2015
  - Re: [Coq-Club] difference between coqchk and Print Assumptions, Enrico Tassi, 03/29/2015
    - Re: [Coq-Club] difference between coqchk and Print Assumptions, Jonathan Leivent, 03/29/2015
      - Re: [Coq-Club] difference between coqchk and Print Assumptions, Arnaud Spiwack, 03/30/2015
        
        Re: [Coq-Club] difference between coqchk and Print Assumptions, Pierre Courtieu, 03/30/2015
        
        Re: [Coq-Club] difference between coqchk and Print Assumptions, Enrico Tassi, 03/30/2015
        
        Re: [Coq-Club] difference between coqchk and Print Assumptions, Pierre-Marie Pédrot, 03/30/2015
        Re: [Coq-Club] difference between coqchk and Print Assumptions, Jonathan Leivent, 03/30/2015