The Coq mailing list

[Hendrik Tews <(e29315a54f%hidden_head%e29315a54f)tews(e29315a54f%hidden_at%e29315a54f)os.inf.tu-dresden.de(e29315a54f%hidden_end%e29315a54f)>]

I am sorry for the late reply, sometimes I don't have the time to
follow this list.

David MENTRE 
<(e29315a54f%hidden_head%e29315a54f)dmentre(e29315a54f%hidden_at%e29315a54f)linux-france.org(e29315a54f%hidden_end%e29315a54f)>
 writes:

   Versions used:
     * The Coq Proof Assistant, version 8.3pl2 (August 2011)
     * ProofGeneral 3.7
     * GNU Emacs 23.3.1
     * System: Ubuntu Linux 11.10 (oneiric)

Proof General in Debian stable, Ubuntu and probably many other
Debian derivatives is completely outdated. However, the package
in Debian testing is up-to-date (prerelease of Proof General 4.2)
and has very light dependencies. You should be able to install
this package after installing mmm-mode.

   I added following lines in my .emacs:
   -----
   ;; For ProofGeneral mode
   (setq coq-version-is-V8-0 nil)
   (setq coq-version-is-V8-1 t)
   (setq coq-prog-name "coqtop")
   (setq coq-load-path '("/usr/local/lib/why3/coq"
                         "/usr/local/lib/why3/coq/int"
                         "/usr/local/lib/why3/coq/real"))

coq-load-path has been added in Proof General 4.1, it has no
effect on older versions. 

     2. I load ProofGeneral with M-x proofgeneral (apparently a Debian
   specific configuration)

This is necessary for Proof General packages 3.7 and earlier. The
new packages don't need this.


Bye,

Hendrik