aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
Diffstat (limited to 'generic')
-rw-r--r--generic/pg-user.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 34afcf0e..2dc04816 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1,6 +1,6 @@
;;; pg-user.el --- User level commands for Proof General
;;
-;; Copyright (C) 2000-2008 LFCS Edinburgh.
+;; Copyright (C) 2000-2009 LFCS Edinburgh.
;; Author: David Aspinall and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -16,6 +16,8 @@
;;; Code:
(require 'span)
+(require 'scomint)
+
(require 'proof) ; loader
(require 'proof-script) ; we build on proof-script