aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorpsteckler2017-05-25 15:10:44 -0400
committerGitHub2017-05-25 15:10:44 -0400
commitb392b77a1e247905fbc0a1cce1a2b494878836b8 (patch)
tree8565b920fb1946fdb69edfbd9a9c61cbcc7ce455 /doc
parent2202c8a405f50dcb589f69db106afcdbdd22cafd (diff)
parentc9e9c691c353d5d4835551de8d7d1f4c0ec74b9f (diff)
Merge pull request #185 from psteckler/remove-contribs
Remove mmm and ML4PG contribs
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi9
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 79694197..945e6821 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4,7 +4,7 @@
@c
@c
@c TODO:
-@c MMM support, Theorem dependencies, history in script and response,
+@c Theorem dependencies, history in script and response,
@c identifier info commands
@@ -5455,7 +5455,7 @@ URL of web page for Isabelle.
-@c FIXME todo: theorem dependencies, MMM
+@c FIXME todo: theorem dependencies
@c =================================================================
@@ -6144,9 +6144,8 @@ Summer Schools. Many new features have been added to enhance Coq mode
Support has been added for the useful Emacs packages Speedbar
@c @uref{http://cedet.sourceforge.net/speedbar.shtml,Speedbar}
-and Index Menu, both usually distributed with Emacs. Compatible
-versions of the Emacs packages Math-Menu (for Unicode symbols) and MMM
-Mode (for multiple modes in one buffer) are bundled with Proof General.
+and Index Menu, both usually distributed with Emacs. A compatible
+version of the Emacs package Math-Menu (for Unicode symbols) is bundled with Proof General.
An experimental Unicode Tokens package has been added which will replace
X-Symbol.