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.

Reply via email to