coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Can useless warnings be switched off?
Date: Mon, 1 Aug 2016 12:03:47 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f65.google.com
Ironport-phdr: 9a23:9daNdhZp5DyjlwdR+wIAniT/LSx+4OfEezUN459isYplN5qZpci4bnLW6fgltlLVR4KTs6sC0LuO9f+9EjVZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxiL35osSbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyBehTCy1jOGQo7uXqswPCRE2B/C1PfH8Rl09jAxLE91nWV5Lq+n/xtvB8w2+WNMjtC7YwcTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

Dear all,

I recently upgraded to coq 8.5pl1. I compiled the one that comes from the arch-linux user repository (https://aur.archlinux.org/packages/coq/). I noticed that when running coq it prints quite a few warnings that look like

<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked.

This happens both when compiling using coqc and it will also prints these warnings to console when stepping through source using coqide. E.g., when stepping over "Require Import NArith" in coqide, it will print four of these warning message. These warnings are not helpful to me so I am wondering if they can be switched off or be disabled in some way. They obscure more useful output that might be present when I 'make' a coq project.

Kind regards,

Chris

[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