Fix type of proof-completed-proof-behaviour.

1 files changed, 5 insertions, 1 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 023bbf2f..2bf24661 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -849,7 +849,11 @@ There is no built-in understanding of the undo behaviour of nested
 proofs; instead there is some support for un-nesting nested proofs in
 the proof-lift-global mechanism.  Of course, this is risky because of
 nested contexts!"
-  :type 'boolean
+  :type '(choice
+	  (const :tag "Close on save only" nil)
+	  (const :tag "Close next command" closeany)
+	  (const :tag "Close next goal" closegoal)
+	  (const :tag "Extend" ignore))
   :group 'proof-script)
 
 (defcustom proof-lift-global nil