aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-auxmodes.el
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-05-24 11:14:51 -0400
committerGravatar Paul Steckler <steck@stecksoft.com>2017-05-24 11:14:51 -0400
commitc9e9c691c353d5d4835551de8d7d1f4c0ec74b9f (patch)
treef89d20d989b309730281d4266b734e0adaed1867 /generic/proof-auxmodes.el
parentafb29a670c537412d09cec703da7e8821c658196 (diff)
Remove mmm and ML4PG contribs and remove references to them in code and docs
Diffstat (limited to 'generic/proof-auxmodes.el')
-rw-r--r--generic/proof-auxmodes.el22
1 files changed, 0 insertions, 22 deletions
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index a6f06479..aa6ddd23 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -15,28 +15,6 @@
;;; Code:
;;
-;; MMM
-;;
-(defun proof-mmm-support-available ()
- "A test to see whether mmm support is available."
- (and
- (or (featurep 'mmm-auto)
- (progn
- ;; put bundled version on load path
- (proof-add-to-load-path
- (concat proof-home-directory "contrib/mmm/"))
- ;; *should* always succeed unless bundled version broken
- (proof-try-require 'mmm-auto)))
- ;; Load prover-specific config in <foo>-mmm.el
- (proof-try-require (proof-ass-sym mmm))))
-
-(proof-eval-when-ready-for-assistant
- (if (and (proof-ass mmm-enable)
- (proof-mmm-support-available))
- (proof-mmm-set-global t)))
-
-
-;;
;; Maths menu
;;
(defun proof-maths-menu-support-available ()