coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/01/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Jason Gross, 08/01/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/02/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Pierre-Marie Pédrot, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Jeehoon Kang, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/03/2016
- RE: [Coq-Club] Can useless warnings be switched off?, Soegtrop, Michael, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Matej Kosik, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Frédéric Besson, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/04/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/18/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Jeehoon Kang, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Ralf Jung, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Pierre-Marie Pédrot, 08/03/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Chris Dams, 08/02/2016
- Re: [Coq-Club] Can useless warnings be switched off?, Jason Gross, 08/01/2016
Archive powered by MHonArc 2.6.18.