coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 14:01:46 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:Xg7x4RRUZjZet89ngjxXh5ceRdpsv+yvbD5Q0YIujvd0So/mwa64YhWN2/xhgRfzUJnB7Loc0qyN4vmmAzJLu8bJ8ChbNscdD1ld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbshsi6n9q/54fUK10RwmHsOPUocl7s/U2R7pBQ2to6bP5pi1PgmThhQ6xu32RmJFaezV7Xx/yb29pdyRlWoO8r7MVaUK/3LOwSRL1cCyk6YShuvJW4/S/qFlTUoyNAGiVLylsbSzTCuRr9R9L6tjbwnut7wiiTe8PsHp4uXjH31a5vRlfKlSEIf2o77WfYoslojedAvwnnoAZwld2HKLqJPeZzK/uONegRQnBMC5sJWg==

I found the old thread:
<https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00168.html>

That explains what I am seeing as being the expected behavior. People
have been asking for suggestions back then, so here they are ;)

> My proposal here would be to only show axioms which are actually used by
> a name exported by one of the modules passed to coqchk. Alternatively,
> Program could provide means of importing the base functionality without
> needlessly importing modules. What do you think?

Kind regards,
Ralf

[Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
- Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
  - Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Beta Ziliani, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Pierre Courtieu, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
        Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Matthieu Sozeau, 08/19/2016