David Aspinall <david.aspin...@ed.ac.uk> writes:
On 08/12/10 16:47, Pierre Courtieu wrote:
> The idea is the following if I understand well.
> A command "Require f" is about to be sent to coq, but *before that* we
> want to perform the following:
> 1) send "Locate Library f"
> 2) wait for the answer of coq: "path/to/f" .
> 3) send "make -C ... path/to/f.vo"
> 4) wait until make finished its job
If possible I would retrac the Locate Library command before
doing step 5.
> 5) finally send the "Require f" to coq if everything went well (error
> Tell me if I am wrong.
No, you are absolutely right.
ProofGeneral-devel mailing list