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.

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to