That's OK with me.
P.

2011/9/14 Hendrik Tews <t...@os.inf.tu-dresden.de>:
> Tom Prince <tom.pri...@ualberta.net> writes:
>
>   >>   Does anybody use -I ... -as ... ?? Does anybody has an opinion
>   >>   about whether Coq Proof General should support -I ... -as ... ??
>
>   If somebody needs it later, we can
>   always add it.
>
> Of course, but I don't want to make an incompatible change, when
> we add -I ... -as ... later.
>
> Given that nobody really needs -I ... -as ..., I suggest to have
> 3 kinds of elements in coq-load-path:
>
> - simple strings for option -I
> - lists of the form ('rec "dir" "path") for -R dir -as path,
>  where path can be omitted for -R dir
> - lists of the form ('nonrec "dir" "path") for -I dir -as path,
>
> Finally, for convenience, elements of the form ("dir") and
> ("dir" "path") are treated as abbreviations of ('rec "dir") and
> ('rec "dir" "path"), respectively.
>
>
> Bye,
>
> Hendrik
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to