Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Axioms reported by coqchk

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk


Chronological Thread 
  • 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 14:16:51 +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:e/TzVhzCAWzTIdXXCy+O+j09IxM/srCxBDY+r6Qd0eMVIJqq85mqBkHD//Il1AaPBtSCragawLCG++C4ACpbsM7H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpqsSVOVsD3mr1Iesrak7n9UOJ7oheqLAhA5558gHOrHpMdrYe7kJTDnXXoSzB4Nyt9oVo6SVatqFp3cdBVaLnY/ZwFuQAX3wQGjtqv4iz6VGDEFPOtTMgVTAdlQMNCAzY5jn7WI3wu230rLlTwi6faO//RqkpVC/nz6ptUh6gqiAaLTIw9imDiMV7lb9Wu1ehqhplwsjWZ5yPOPN4VqXaZ9YTQWdaQ94XUDZOVNDvJ7ATBvYMaL4L57L2oEED+EbmCA==



On 08/19/2016 02:01 PM, Ralf Jung wrote:
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.

Names which are not exported are still available via qualified names when importing the module, so this makes sense to include them in the list (i.e., if you are allowed to import the module, then you get the power to use these axioms).

Alternatively,
Program could provide means of importing the base functionality without
needlessly importing modules. What do you think?

But then how different is this from refine ?

Kind regards,
Ralf




Archive powered by MHonArc 2.6.18.

Top of Page