Tom Prince <> writes:

   On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews <> 
   > * 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.


ProofGeneral-devel mailing list

Reply via email to