aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-goals.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r--generic/pg-goals.el1
1 files changed, 1 insertions, 0 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index d9a350ec..37862a64 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -20,6 +20,7 @@
(eval-when-compile
(require 'easymenu) ; easy-menu-add, etc
(require 'span)) ; span-*
+(require 'proof-script) ;For proof-insert-sendback-command
(defvar proof-goals-mode-menu) ; defined by macro below
(defvar proof-assistant-menu) ; defined by macro in proof-menu