The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Thanks Jason! It is good to know that it will be possible to remove these warnings in the future.

2016-08-01 19:42 GMT+02:00 Jason Gross <jagro AT google.com>:

This feature will be available in Coq 8.6, with the -w flag.  (as, e.g., -w "-deprecated-appcontext -notation-overridden")  I don't believe there are plans to backport it to 8.5.

On Mon, Aug 1, 2016 at 3:03 AM Chris Dams <chris.dams.nl AT gmail.com> wrote:

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