coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] difference between coqchk and Print Assumptions
Date: Sun, 29 Mar 2015 19:41:31 +0200

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,
--
Enrico Tassi

[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