coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Emacs: MMM mode with Proof General

From: "N. Raghavendra" <raghu AT hri.res.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] Emacs: MMM mode with Proof General
Date: Sun, 13 Sep 2015 08:26:55 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=raghu AT hri.res.in; spf=Pass smtp.mailfrom=gsmlcc-coq-club AT m.gmane.org; spf=Pass smtp.helo=postmaster AT plane.gmane.org
Cancel-lock: sha1:uSoGO4by9hLf2e/3u60eiHJJJDc=
Ironport-phdr: 9a23:s+cjNxNAICOkXl8npDcl6mtUPXoX/o7sNwtQ0KIMzox0KPT5rarrMEGX3/hxlliBBdydsKIYzbCP+PmxCCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkbrrsMSCMk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQdwaX4mogVTBctFwAOQHK7BjkU5H9qCKw/r5n0SaaIOX2V7FyQzm5qaZtHkzGkiACYnQftintg8NwhbxWph67rlY3l5Tdb4GIHPpkf+XHcMhcRGwXDZUZbDBIHo7pN9hHNOEGJ+sN94Q=

I am unable to get MMM mode to work with Proof General and Coq. I've
done

(add-to-list 'load-path "/pkg/proof-general/contrib/mmm")
(add-to-list 'load-path "/pkg/proof-general/coq")
(require 'coq-mmm)

but nothing happens. That is, there is no change of mode or
fontification when I pass from a Coq part of the buffer to a Coqdoc HTML
or LaTeX part of the buffer. I'd be grateful if someone can provide me
some directions.

Cheers,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Emacs: MMM mode with Proof General, N. Raghavendra, 09/13/2015