So your answer is no? One cannot communicate with the prover from inside proof-shell-insert-hook?
No, do not do that.
There might be some misunderstanding: I want to use "Locate Library" only to map a library names to a file path. This mapping depends on coq's LoadPath, which can be changed with command line switches or with the various LoadPath commands at runtime.
I think I understood, roughly, but thanks for clarifying, I think the coqdep stuff was just a failed attempt to do this (maybe before Locate Library was available).
- D. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
