coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 15:16:55 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jacques-henri.jourdan AT normalesup.org; spf=Neutral smtp.mailfrom=jacques-henri.jourdan AT normalesup.org; spf=None smtp.helo=postmaster AT ulminfo.fr
Ironport-phdr: 9a23:ack0+xyHM0KViNfXCy+O+j09IxM/srCxBDY+r6Qd0e0fIJqq85mqBkHD//Il1AaPBtSCragawLeL++C4ACpbsM7H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpqsSVOVsD2Wf1Iesrak7n9UOJ7oheqLAhA5558gHOrHpMdrYe7kJTDnXXoSzB4Nyt9oVo6SVatqFp3cdBVaLnY/ZwFuQAX3x1e1wyscbsrFzISRaFznoaSGQf1BRSUCbf6xSvfJ76qzb3ra9d1S+APIXUSq0uVT2kp/NpQRTxlSoccj409nvWzM53kbhXqRSJoRtlxofQbZqILLx5ZKyLLoBSfnZIQssED38JOYi7dYZaV+c=

On 08/19/2016 03:13 PM, Ralf Jung wrote:

However, if "--list-dependencies-of" would take wildcards, like "iris.*"
that could work.. oh wait, no. That would also cover all the reexported
unused axioms from the standard library, right?

That was the kind of think I was thinking about. And no, I do not think you can access an stdlib axiom via iris qualified names.

[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
        Re: [Coq-Club] Axioms reported by coqchk, Ralf Jung, 08/19/2016
        Re: [Coq-Club] Axioms reported by coqchk, Pierre-Marie Pédrot, 08/19/2016
        
        RE: [Coq-Club] Axioms reported by coqchk, Soegtrop, Michael, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Jacques-Henri Jourdan, 08/19/2016
    - Re: [Coq-Club] Axioms reported by coqchk, Robbert Krebbers, 08/19/2016
      - Re: [Coq-Club] Axioms reported by coqchk, Guillaume Melquiond, 08/19/2016
        
        Re: [Coq-Club] Axioms reported by coqchk, Robbert Krebbers, 08/19/2016