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

Reply via email to