aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-custom.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-29 09:48:07 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-29 09:48:07 +0000
commit7c81d76b3277256f596ed7cd102ab9fbff4d98ff (patch)
tree4029c0720c6673bead0bf90bee15103eb4b5ae28 /generic/pg-custom.el
parentdf953a00561ee47fbb2ca09c1985a67f47591fb3 (diff)
Move proof-experimental-features back and make it constant.
Diffstat (limited to 'generic/pg-custom.el')
-rw-r--r--generic/pg-custom.el21
1 files changed, 0 insertions, 21 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index b73ef30e..2f9ef2f4 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -182,27 +182,6 @@ http://proofgeneral.inf.ed.ac.uk/trac"
:type 'file
:group 'prover-config)
-;;;
-;;; Experimental features: not a per-prover settings,
-;;; but initialised here because of default value's
-;;;; dependency on proof-general-version
-
-(defcustom proof-experimental-features
- (if (string-match "pre" proof-general-version) t)
- "*Whether to enable certain features regarded as experimental.
-Proof General includes a few features designated as \"experimental\".
-Enabling these will usually have no detrimental effects on using PG,
-but the features themselves may be buggy.
-
-We encourage users to set this flag and test the features, but being
-aware that the features may be buggy (problem reports and
-suggestions for improvements are welcomed).
-
-In the current 3.7 release, there are no features classed as experimental
-so this option is set by default."
- :type 'boolean
- :group 'proof-user-options)
-
(provide 'pg-custom)