coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Axioms reported by coqchk

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 15:38:34 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:18QglxPtk6OciWSr1PUl6mtUPXoX/o7sNwtQ0KIMzox0KPryrarrMEGX3/hxlliBBdydsKMdzbCI+P69ESxYuNDa4ShEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9GO35F8bogtit0KjqotuIMlwO3mT2P+46bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4BLEVE6E4mYWemQQiBtBRQbfvz/gWZKkiCzwvOdnxGG5J8D8R70uQnz26q5qTB7uhyMGLCIi2HvQgMZ9lr5Yuh+rrRFl2MjSZNfGZ7JFYqrBcIZCFiJ6VcFLWnkZDw==

On 08/19/2016 03:29 PM, Guillaume Melquiond wrote:

> However, just importing Coq.Program.Syntax is enough.

This is kind of baffling: for some reason, requiring Program.Syntax
transitively causes Program.Tactics to be required.

You are right. No idea where it comes from exactly.

Anyway, it seems that importing Coq.Program.Tactics is enough to make the Program vernacular to work without coqchk reporting on any axioms.

The culprit is Coq.Program.Equality, which does not seem to be needed.

Re: [Coq-Club] Axioms reported by coqchk, (continued)
- 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