Tom Prince <tom.pri...@ualberta.net> writes:

   On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews <t...@os.inf.tu-dresden.de> 
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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to