Tom Prince <> 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

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.


ProofGeneral-devel mailing list

Reply via email to