So your answer is no? One cannot communicate with the prover from
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).
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.