2011/1/13 Hendrik Tews <t...@os.inf.tu-dresden.de>
> Pierre Courtieu <pierre.court...@cnam.fr> writes:
> invisble command. However LoadPath is probably not part of the undo model
> and Coq does not retract them when going back to a previous state.
> I just tried, changes in the LoadPath are not undone by
> Backtrack. This basically means that when changing the active
> scripting buffer we have to restart coqtop. It also means we can
> stop this discussion.
If you really think it could be useful I may implement this as an option in
I hope that
> *** Local Variables: ***
> *** coq-load-path: ("../../ALEA/src") ***
> *** End: ***
> will be sufficient. The -I arguments can be derived from
> coq-load-path and coqtop is default.
That would be nice. For this we can ask David to allow prog-args to be a
function instead of a list. In proof-shell near line 239. This way we can
define coq-prog-args as the function that build the -I list from
ProofGeneral-devel mailing list