Tom Prince <[email protected]> writes:
On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews <[email protected]>
wrote:
> * 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.
-R only accepts two options, not a single one.
I see
blau ~ 4> coqc -help
Usage: coqc <options> <Coq options> file...
options are:
-verbose compile verbosely
-image f specify an alternative executable for Coq
-t keep temporary files
Coq options are:
-I dir -as coqdir map physical dir to logical coqdir
-I dir map directory dir to the empty logical path
-include dir (idem)
-R dir -as coqdir recursively map physical dir to logical coqdir
-R dir coqdir (idem)
And the reference manual lists only -R dir -as coqdir.
> Does anybody use -I ... -as ... ?? Does anybody has an opinion
> about whether Coq Proof General should support -I ... -as ... ??
I suspect that it isn't worth it. If there are no subdirectories,
-R ... ... and -I ... -as ... have the same effect.
Sure, but if there are subdirectories, the effect is different.
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
