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:12:05 +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:CgFnaRCahiFaMHnmdhf5UyQJP3N1i/DPJgcQr6AfoPdwSP79rsbcNUDSrc9gkEXOFd2CrakV0qyM7eu9BCRAuc/H6yFaNsQUFlcssoY/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbtr8FoOatcmrzef6o8SVOFQRwmDjKu4vZFXu9EOK55FQ2dMjYo8KiTLx6kNSfOpXwW46bXmypD3bovmKwZh47i5LsOgg/cMTGY/zfqA/UKAKRG9+azN9t4XXskzIShLK7X8BWE0XlABJCk7L9kLURJD05xH9vOBwwjXSHtf7R7o5Qy/qu6JiSRvpjigDNiUl60nNjcZ6gbhHowisrRZy2ZWSZoXDZ6k2Rb/UYd5PHTkJZc1WTSEUWo4=

On 08/19/2016 02:16 PM, Jacques-Henri Jourdan wrote:

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 ?

It seems that just importing

From Coq.Program Require Import Syntax.

is enough to make the Program vernacular to work. As far as I see, the above does not import any axioms, contrary to importing Coq.Program.Tactics.

Some remarks:

- Everything in Coq.Program.Syntax and Coq.Program.Basics seems to be very generic and is not specific to Program at all. Why isn't that somewhere in Coq.Prelude?

- When using Program without importing anything, Coq complains with

"Error: Library Coq.Program.Tactics has to be required first."

However, just importing Coq.Program.Syntax is enough. Why is one required to import anything of Program from the standard library to use the Program vernacular?

Re: [Coq-Club] Axioms reported by coqchk, (continued)