Tom Prince <tom.pri...@ualberta.net> writes:
On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews <t...@os.inf.tu-dresden.de>
> * 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.
blau ~ 4> coqc -help
Usage: coqc <options> <Coq options> file...
-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.
ProofGeneral-devel mailing list