The Coq mailing list

[Anton Podkopaev <anton AT podkopaev.net>]

Hello!

Short:

Does anyone have a script to turn 'Suggest Proof Using' output at Qed to an actual

'Proof using ... .' directive in .v files?

A related issue at GitHub: https://github.com/coq/coq/issues/7877

Long:

We have a relatively big project in Coq which we would like to type check in parallel.

However, we have an obstacle: we use the section mechanism a lot in the project, and 

it breaks parallel compilation [Comment1].

A solution I know for the problem is to introduce 'Proof using' annotations suggested by

'Suggest Proof Using' for proofs in the project.

I wonder if there is an automated way to introduce them.

[Comment 1]

Coq doesn't know a lemma's type (i.e. does the lemma depends on a section's variable or not)

until it checks the lemma's proof. As a result, it cannot type check other facts depending on

the lemma in parallel w/ checking the lemma's proof.

thanks,

Anton Podkopaev

podkopaev.net