From c9e9c691c353d5d4835551de8d7d1f4c0ec74b9f Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 24 May 2017 11:14:51 -0400
Subject: Remove mmm and ML4PG contribs and remove references to them in code
 and docs

---
 lib/holes.el  | 7 +++----
 lib/pg-dev.el | 4 ++--
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/holes.el b/lib/holes.el
index c0a864b0..38a90cfb 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -599,10 +599,9 @@ created.  Return the number of holes created."
   "Default hook after a skeleton insertion: put holes at each interesting position."
   ;; Not all versions of skeleton provide `skeleton-positions' and the
   ;; corresponding @ operation :-(
-  (unless (boundp 'mmm-inside-insert-by-key) ; pc: this hack is ok for me
-    (when (boundp 'skeleton-positions)
-      (dolist (pos skeleton-positions)	;; put holes here
-	(holes-set-make-active-hole pos pos)))))
+  (when (boundp 'skeleton-positions)
+    (dolist (pos skeleton-positions)	;; put holes here
+      (holes-set-make-active-hole pos pos))))
 
 (defconst holes-jump-doc
   (concat "Hit \\[holes-set-point-next-hole-destroy] to jump "
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index e11d15ff..758b3d51 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.el
@@ -101,13 +101,13 @@
    '(proof-splash pg-assoc pg-xml proof-depends proof-indent proof-site
      proof-shell proof-menu pg-pbrpm pg-pgip proof-script
      proof-autoloads pg-response pg-goals proof-toolbar
-     proof-easy-config proof-config proof-mmm proof
+     proof-easy-config proof-config proof
      proof-utils proof-syntax pg-user pg-custom
      proof-maths-menu proof-unicode-tokens
      pg-thymodes pg-autotest
      ;;
      isar-syntax isar-find-theorems isar-unicode-tokens
-     isar-autotest interface-setup isabelle-system isar isar-mmm
+     isar-autotest interface-setup isabelle-system isar 
      isar-keywords
      ;;
      coq-abbrev coq-db coq-unicode-tokens coq-local-vars coq coq-syntax
-- 
cgit v1.2.3