coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Get rid of "suggest Proof using" warning in new Proof General

From: Xuanrui Qi <xuanrui AT nagoya-u.jp>
To: coq-club AT inria.fr
Subject: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General
Date: Thu, 21 May 2020 16:15:18 +0900
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xuanrui AT nagoya-u.jp; spf=Pass smtp.mailfrom=xuanrui AT nagoya-u.jp; spf=None smtp.helo=postmaster AT smtp.nagoya-u.jp
Ironport-phdr: 9a23:StcxsBMP4AQiSweTPgUl6mtUPXoX/o7sNwtQ0KIMzox0LfX4rarrMEGX3/hxlliBBdydt6sZzbOP6+u5ADBIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLN/IA+roQnMqsUajpZuJrs+xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuBGvqQF/zYDKbo+aKPRxcazSc94BWWpMXdxcWzBdDo6mbYYCCfcKM+ZCr4n6olsDtRqxBRS2C+Pp0D9Im3721rAh3eQgDArL2wMhH88Uv3TSttX1KaYSXPuzzKbSwjXDaPNX1i3k5IjVaBwho+mMUKt2fMHMxkYhCxnLgU+MqYz5ITyVzOINvnCG4+dhSe+ihXAqpQ5vrzWtyMkgl4bHiI0VxF3Y6Sl13Zg5KcG8RUN7b9CpEoZcuSGbOoZ2Qc4vQm9ltSUmxrMJv5OwYSsEyIw/yhLCZfGKfZKE7xP5WOqMIjp0mmhpdbGxihqq7ESs1OPxWtOp3FpQsyZJjsPAum0O2hDN7MWMV+Fz8V272TmV0gDe8uFELl4wlarcM5Mh2bswloYLsUjZGC/5gkr2jKiWd0o+4+So9v7rYrf+ppOENo90jB/xMrg2l8CiD+k1PBICUmmB9eih17Dv41f1TbZEg/Eul6nWqpHaJcAVpq6jBA9V154u6hmiDzi81tQYh2QHLFNedRKBlYfpNFbOIfDiAvumnlSgijVrx+jeMr37HprNNmTDkKvmfbtl90FczxMzwclD6JJQF7EOO+n+WlTxtdzdFh82KRa4w+fhCNVn14MRQ3iDAqGDMPCajVjd7eU2ZuKIeYU9uTDnKvFj6eS9o2U+nAotYKCvx4YWIEm5VqB2Pkyfe2ftqtEIHmAbt08jCu7y3g7RGQVPbmq/CvpvrgowD5irWN+aG9KdxYeZ1SL+JaV4I2BLDlfVQSXzcpmcHfEFZyWDK4p81D4cB+D4F90RkCq2vQq/8IJJa/LO83RD55Tq299k7qjO0xMqp2QtXpatllqVRmQxpVsmAjo/3aRxu0t4kwzR16F3hO1RUMEV5esbCwo=

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

[Coq-Club] Get rid of "suggest Proof using" warning in new Proof General, Xuanrui Qi, 05/21/2020
- Re: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General, Pierre Courtieu, 05/24/2020
  - Re: [Coq-Club] Get rid of "suggest Proof using" warning in new Proof General, Pierre Courtieu, 05/26/2020