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
