Tom Prince writes:
Some developments don't fully qualify their imports, and so coqdep gives
warning about ambiguous imports. Allow these developments to use
auto-compilation mode anyway.
Could you describe an example? What is coqdep printing in these
cases?
-(if (string-match "^
Tom Prince writes:
On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews
wrote:
> * 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 opti
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.
What do you think about -I ... -as ... ? Do people use it?
Bye,
Hendrik
__
OK. I have uploaded a small patch in Trac.
Kind regards,
Erik
On 09/11/2011 06:00 PM, Pierre Courtieu wrote:
OK now I understand, and agree. Added a trac.
Thanks for reporting!
P
--
Érik Martin-Dorel
PhD student, ENS de Lyon, LIP
http://perso.ens-lyon.fr/erik.martin-dorel/
Hello,
On 09/11/2011 04:30 PM, Tom Prince wrote:
On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu
wrote:
2011/9/10 Erik Martin-Dorel:
1. Now the behavior of [C-x C-c] is not really consistent with the one of
[C-c C-x].
Indeed, the second command calls yes-or-no-p before killing the
prover
On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu
wrote:
> 2011/9/10 Erik Martin-Dorel :
> > 1. Now the behavior of [C-x C-c] is not really consistent with the one of
> > [C-c C-x].
> > Indeed, the second command calls yes-or-no-p before killing the
> > prover, while the first one now exits Ema
On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews
wrote:
> * 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.
> Does any
Some developments don't fully qualify their imports, and so coqdep gives
warning about ambiguous imports. Allow these developments to use
auto-compilation mode anyway.
Signed-off-by: Tom Prince
---
ProofGeneral-4.1RC4/coq/coq.el |5 -
1 files changed, 4 insertions(+), 1 deletions(-)
dif
Since we are approaching the next official Isabelle release (probably
October 2011), this is the same procedure as everytime.
Is there any serious release schedule for PG 4.1?
Just before Isabelle2011 it was planned to happen within a few days before
our release, then new features came it. No
2011/9/10 Erik Martin-Dorel :
> Hi,
>
> I would like to report three interrelated issues that I noticed in the
> current CVS version of ProofGeneral.
>
>
>
> 1. Now the behavior of [C-x C-c] is not really consistent with the one of
> [C-c C-x].
> Indeed, the second command calls ye
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?).
Bye,
Pierre Courtieu
2011/9/9 Hendrik Tews :
> Tom Prince writes:
>
> Make coq-load-path accept either strings (which are passed "-I" options)
> or
11 matches
Mail list logo
