The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

> [...] why do you put a lemma in a section if it uses no section variables

For [Local] behavior


On Mon, Mar 23, 2015 at 8:00 AM, Enrico Tassi 
<enrico.tassi AT inria.fr>
 wrote:
> On Mon, Mar 23, 2015 at 12:29:16AM -0400, Jason Gross wrote:
>> Sometimes, [Set Suggest Proof Using] suggests [Proof using .], and
>> sometimes, it suggests [Proof using Type.].  The reference manual seems to
>> indicate that they are the same.  Is there a difference between them, and,
>> if not, why does [Set Suggest Proof Using] sometimes choose one and
>> sometimes choose the other?
>
> They do work the same: the system uses only the variables occurring in
> the statement.  I'd say the doc is correct.
>
> The code suggests "Proof using." when the section is empty (or the lemma
> uses no section hyps), and "Proof using Type." when all the used
> variables occur in the statement.
>
> The behavior of "Suggest..." is not intended.  At some point the two
> syntaxes had different meaning, but then I changed my mind.
>
> Still the current behavior could be of some use: why do you put a lemma
> in a section if it uses no section variables?  Maybe "Suggest..." should
> always print "..using." instead of "..Type." and give a warning in case
> the lemma has no reason to be in the section?  What do you think?
>
> Thanks for spotting this one!
> --
> Enrico Tassi
>