The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello,

2012/4/3 David MENTRE 
<dmentre AT linux-france.org>:
> 2012/4/3 Jelle Herold 
> <jelle AT defekt.nl>:
>> I'm not entirely shure what the problem is, these are rather old versions 
>> of
>> PG and coq

As a follow-up: as suggested by Jelle and also privately, I have
manually installed a more recent ProofGeneral 4.1. Using following
lines in my .emacs, it works like a charm:
----
;; For PG 4.1
(load-file "/home/david/install/ProofGeneral/generic/proof-site.el")
(setq coq-load-path '(("/usr/local/lib/why3/coq/real" "Why3.real")
                      ("/usr/local/lib/why3/coq/int" "Why3.int")))
----

Many thanks!

Best regards,
d.