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
