aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el8
1 files changed, 0 insertions, 8 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 2c2c760d..2db38563 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -969,14 +969,6 @@ retracted using `proof-auto-retract-dependencies'."
;; taken when scripting is turned off/on.
;;
-(defconst proof-no-fully-processed-buffer nil
- "Set to t if buffers should always retract before scripting elsewhere.
-Leave at nil if fully processd buffers make sense for the current proof
-assistant. If nil the user can choose to fully assert a buffer when
-starting scripting in a different buffer. If t there is only to choice
-to fully retract the active buffer before starting scripting in a different
-buffer. This last behavior is needed for Coq.")
-
(defun proof-protected-process-or-retract (action &optional buffer)
"If ACTION='process, process, If ACTION='retract, retract.
Process or retract the current buffer, which should be the active