aboutsummaryrefslogtreecommitdiff
path: root/generic/pg-custom.el
diff options
context:
space:
mode:
authorPaul Steckler2017-05-24 11:14:51 -0400
committerPaul Steckler2017-05-24 11:14:51 -0400
commitc9e9c691c353d5d4835551de8d7d1f4c0ec74b9f (patch)
treef89d20d989b309730281d4266b734e0adaed1867 /generic/pg-custom.el
parentafb29a670c537412d09cec703da7e8821c658196 (diff)
Remove mmm and ML4PG contribs and remove references to them in code and docs
Diffstat (limited to 'generic/pg-custom.el')
-rw-r--r--generic/pg-custom.el11
1 files changed, 0 insertions, 11 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 2edf320e..0956f970 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -194,17 +194,6 @@ Currently this setting is UNIMPLEMENTED, changes have no effect."
:set 'proof-set-value
:group 'proof-user-options)
-(defpgcustom mmm-enable nil
- "*Whether to use MMM Mode in Proof General for this assistant.
-MMM Mode allows multiple modes to be used in the same buffer.
-If you activate this variable, whether or not you really get MMM
-support depends on whether your proof assistant supports it."
- :type 'boolean
- :set 'proof-set-value
- :group 'proof-user-options)
-
-
-
(provide 'pg-custom)
;;; pg-custom.el ends here