The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

I have just used the "generalize foo at i j k ..." tactic form for the
first time (well, I think it's the first time I've used it, anyway). I
used it to solve a problem with dependent types that I couldn't see any
other reasonable way to solve. Now that I've actually used it, I am
relieved to finally understand how the random-looking list of numbers
one finds at the end of generalize ... at ... tactics can be rationally
arrived at. And, indeed, the numbers at the end of its cousin,
pattern ... at ... (e.g. in le_uniqueness_proof in the Coq FAQ).

I am interested to know in what situations other people use these
particular variants of generalize and pattern - I wonder if I should be
using them more often.
-- 
Robin