From de4e4aa641e8782f7a88d402ab380d4d94f4ef96 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 16 Nov 1999 21:01:50 +0000
Subject: Fix type of proof-completed-proof-behaviour.

---
 generic/proof-config.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3