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

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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to