aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/ProofGeneral.texi9
-rw-r--r--generic/proof-useropts.el7
2 files changed, 0 insertions, 16 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 0f3ef7ef..b6dcc957 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3246,15 +3246,6 @@ you a reprimand!).
The default value is @code{retract}.
@end defopt
-@c TEXI DOCSTRING MAGIC: proof-allow-undo-in-read-only
-@defopt proof-allow-undo-in-read-only
-Whether Proof General allows text undo in the read-only region.@*
-If non-nil, undo will allow altering of processed text.
-If nil, undo is blocked if the next undo is in processed text.
-
-The default value is @code{nil}.
-@end defopt
-
@c TEXI DOCSTRING MAGIC: proof-query-file-save-when-activating-scripting
@defopt proof-query-file-save-when-activating-scripting
If non-nil, query user to save files when activating scripting.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 07d0464e..be52f32f 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -131,13 +131,6 @@ you a reprimand!)."
:set 'proof-set-value
:group 'proof-user-options)
-(defcustom proof-allow-undo-in-read-only nil
- "*Whether Proof General allows text undo in the read-only region.
-If non-nil, undo will allow altering of processed text.
-If nil, undo is blocked if the next undo is in processed text."
- :type 'boolean
- :group 'proof-user-options)
-
(defcustom proof-three-window-enable nil
"*Whether response and goals buffers have dedicated windows.
If non-nil, Emacs windows displaying messages from the prover will not