> This is, however, not the expected simplification. I decided for > this simple change, because it keeps the functionality of other > proof assistants without that I have to touch their code.
This sounds wise, and what Pierre originally suggested, although if I've followed it seems as if that's not compatible with his convention of setting coq-prog-args in file local variables. - D. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
