That's OK with me. P.
2011/9/14 Hendrik Tews <[email protected]>: > Tom Prince <[email protected]> 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 > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
