> 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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to