aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light
diff options
context:
space:
mode:
Diffstat (limited to 'hol-light')
-rw-r--r--hol-light/hol-light-autotest.el6
1 files changed, 2 insertions, 4 deletions
diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
index b9924c41..5c1cb011 100644
--- a/hol-light/hol-light-autotest.el
+++ b/hol-light/hol-light-autotest.el
@@ -8,10 +8,8 @@
(eval-when-compile
(require 'cl))
-(eval-when-compile
- (require 'proof-site)
- (proof-ready-for-assistant 'coq)
- (defvar coq-compile-before-require nil))
+(require 'proof-site)
+(proof-ready-for-assistant 'hol-light)
(require 'pg-autotest)