The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/07/2015 04:55 PM, Jason Gross wrote:
> ..  If you want
> to do this on the first run of the file, too, you must use [Proof using
> <variables to be used in the proof>].

I guess I don't understand the behavior of [Proof using]:  How is [Proof 
using] important to proof parallelism, if the [Proof using] declaration 
is only processed at Qed time (to determine if the proof obeyed the 
restriction or not, and to abstract over only the used variables)?  Was 
[Proof using] changed in 8.5 to do earlier processing?

-- Jonathan