diff options
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r-- | generic/pg-goals.el | 1 |
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 |