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 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 ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel