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
   > otherwise).
   > Tell me if I am wrong.

No, you are absolutely right.


ProofGeneral-devel mailing list

Reply via email to