Pierre Courtieu <pierre.court...@cnam.fr> writes:

   2011/1/13 David Aspinall <david.aspin...@ed.ac.uk>

   > I suppose Pierre means that you need a way to influence the command line
   > calculation as you wanted, perhaps with yet another control function/hook 
   > variable for prog-args (already several added for Coq..).

OK, I got it now. prog-args becomes a function and for coq it
appends (the value of) coq-prog-args and the contents of
coq-load-path (the latter interspersed with -I's).

If one of you wants to do this, please do, I am busy enough with
other stuff. You might want to use the function

   That's exactly what I mean, but i thing Hendrik wants to use Add LoadPath

No, restarting coqtop on every buffer change and passing
coq-load-path as -I options to coqtop is fine with me. 


ProofGeneral-devel mailing list

Reply via email to