From fcd935b7a2713230349e70f1a13dc6ca0a29fe7c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 7 Aug 2009 14:40:00 +0000
Subject: Fix pareno

---
 generic/pg-user.el | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/generic/pg-user.el b/generic/pg-user.el
index dde8c81f..32f554e1 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -847,19 +847,16 @@ If NUM is negative, move upwards.  Return new span."
    (list (vector
 	  "Undo"
 	  (list 'pg-span-undo span) t))
-   (if proof-experimental-features
-       (list (vector
-	      "Move up"     (list 'pg-move-span-contents span -1)
-	      (pg-numth-span-higher-or-lower (pg-control-span-of span) -1 'noerr))))
-   (if proof-experimental-features
-       (list (vector
-	      "Move down"   (list 'pg-move-span-contents span 1)
-	      (pg-numth-span-higher-or-lower (pg-control-span-of span) 1 'noerr))))
-   (if proof-script-span-context-menu-extensions
-       (funcall proof-script-span-context-menu-extensions span idiom name))
-   (if (and proof-experimental-features
-	    proof-shell-theorem-dependency-list-regexp)
-       (proof-dependency-in-span-context-menu span))))
+   (list (vector
+	  "Move up"     (list 'pg-move-span-contents span -1)
+	  (pg-numth-span-higher-or-lower (pg-control-span-of span) -1 'noerr))))
+  (list (vector
+	 "Move down"   (list 'pg-move-span-contents span 1)
+	 (pg-numth-span-higher-or-lower (pg-control-span-of span) 1 'noerr)))
+  (if proof-script-span-context-menu-extensions
+      (funcall proof-script-span-context-menu-extensions span idiom name))
+  (if proof-shell-theorem-dependency-list-regexp
+      (proof-dependency-in-span-context-menu span)))
 
 (defun pg-span-undo (span)
   "Undo to the start of the given SPAN."
-- 
cgit v1.2.3