Tom Prince <tom.pri...@ualberta.net> writes: Make coq-load-path accept either strings (which are passed "-I" options) or conses of strings (which are passed as "-R" options).
Thanks a lot for your patch. This has been on my todo list, however, I never looked at this point, because I don't use -R (yet). Before I commit your patch to the repository, I would like to discuss the following two points: * Proof General 4.1 will be released shortly (hopefully). I don't know if the policy permits commits with new minor features. David, could you comment on this? Probably a fair portion of the Coq users would benefit from the patch. The patch is very small and can be easily tested. Therefore, I would be in favor of committing the patch, although Proof General is already deeply frozen. * With the patch, coq-load-path covers the options -I and -R ... -as ... With a minor change we will also get -R ... However, -I ... -as ... would still be unsupported. Does anybody use -I ... -as ... ?? Does anybody has an opinion about whether Coq Proof General should support -I ... -as ... ?? [The point here is not the implementation, which would be very simple. The point is, if and how to encode -I ... -as ... in coq-load-path.] Note that Tom's patch does not apply cleanly to cvs head any more. When reading the patch I spotted some errors in the documentation strings, which I fixed a few minutes ago. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
