2011/1/13 Hendrik Tews <[email protected]>
> Pierre Courtieu <[email protected]> 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
coq.
> ...
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
coq-load-path.
P.
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
