Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Can useless warnings be switched off?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can useless warnings be switched off?


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Can useless warnings be switched off?
  • Date: Wed, 3 Aug 2016 10:10:23 +0200

On 02/08/2016 13:14, Chris Dams wrote:
> Thanks Jason! It is good to know that it will be possible to remove
> these warnings in the future.

Those warnings are not produced by Coq, but rather by CAMLP4/5, and
therefore the warning mechanism is useless here.

Warnings cannot be turned off in CAMLP4 because the relevant API has
been missing for ages, whereas it is possible in CAMLP5 (if they appear
in Coq otherwise it's a bug, and it may well be one in your example). In
any case, I advise you to switch to CAMLP5 if you didn't do so already.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page