The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

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