The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

If proofgeneral gives this message outside of a section this is a bug:
it is supposed to be triggered by coq warning, which only happens
inside sections. Please report it here:
https://github.com/ProofGeneral/PG/issues.

To answer your question: you can either go to the menu: Coq / proof
using / never". Or do what is described in the CHANGES file and copied
below.

That said you are right the message is too noisy.

Best
Pierre
----------------8X--------------------------
PG now supports the "Suggest Proof Using" by inserting
(automatically or by contextual menu or by a command) the "Proof
using" annotation suggested by Coq. This suggestion happens at
"Qed" command. By default PG will only highlight the corresponding
"Proof" keyword and let the user actively ask for insertion.

You can customize this behaviour by setting the
coq-accept-proof-using-suggestion to one of these values: 'always,
'highlight, 'ask, 'never. This is also settable from Coq menu. See
documentation of this variable for an explanation of the different
possible values and some more information.


Le jeu. 21 mai 2020 à 09:15, Xuanrui Qi <xuanrui AT nagoya-u.jp> a écrit :
>
> Hi Coq-Clubbers,
>
> A quick question for Proof General users: the latest versions of PG
> gives me a warning if I use `Proof` instead of `Proof using`:
>
> "Proof using" not set. M-x coq-insert-suggested-dependency or right
> click to add it. See also ‘coq-accept-proof-using-suggestion
>
> Since I don't have any section variables, there's no point in doing
> `Proof using`. Is there any way to disable this persistent warning,
> which can be quite annoying?
>
> Best,
> Xuanrui
>