coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre-Marie Pédrot <pierre-marie.pedrot 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:50:02 +0200

On 30/03/2015 13:48, Enrico Tassi wrote:
> 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.

Be aware that it is bugged, so that some care has to be taken.

https://coq.inria.fr/bugs/show_bug.cgi?id=3948

The bug seems to appear because of module trickery, and the checker acts
notably differently from coqtop in this respect, so that it may go
through just fine, but still. The checker is the checker!

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[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