aboutsummaryrefslogtreecommitdiff
path: root/generic/pg-custom.el
diff options
context:
space:
mode:
authorpsteckler2017-05-25 15:10:44 -0400
committerGitHub2017-05-25 15:10:44 -0400
commitb392b77a1e247905fbc0a1cce1a2b494878836b8 (patch)
tree8565b920fb1946fdb69edfbd9a9c61cbcc7ce455 /generic/pg-custom.el
parent2202c8a405f50dcb589f69db106afcdbdd22cafd (diff)
parentc9e9c691c353d5d4835551de8d7d1f4c0ec74b9f (diff)
Merge pull request #185 from psteckler/remove-contribs
Remove mmm and ML4PG contribs
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