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: Mon, 30 Mar 2015 13:48:02 +0200

On Mon, Mar 30, 2015 at 01:33:44PM +0200, Pierre Courtieu wrote:
> Indeed the -o option here is not precise enough.
>
> would it make sense to submitting a feature wish for some [coqchk
> -print-assumptions-for foo] option?

Yep. A pull request would even be better ;-)

The code implementing the recursive traversal and looking for axioms
is in library/assumptions.ml, but I don't know if it can be reused as
such in the checker.

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