On Mon, 12 Sep 2011 08:06:23 +0200, Hendrik Tews <t...@os.inf.tu-dresden.de> 
wrote:
> 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 ... ??
> 
>    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.

Unless somebody else chimes in I would say we shouldn't bother.
If somebody has hierarchy of coq directories, to give an explicit name
to one, I can't imagine that they wouldn't want the directory hierarchy
reflected in the coq hierarchy. If somebody needs it later, we can
always add it.

On Mon, 12 Sep 2011 08:01:35 +0200, Hendrik Tews <t...@os.inf.tu-dresden.de> 
wrote:
>    
>    I am also in favor of releasing this patch, as it doeas not seem ro
>    break the users old configuration settings using coq-prog-args (does
>    it?).
>    
> No, as long as coq-compile-before-require is nil.
It actually only affected me (and seemed to work) with
coq-compile-before-require was t. 
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to