From 98f2e463287e3562dc7b7126e062919a8604ca4a Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Sat, 25 Feb 2017 19:35:35 -0500
Subject: Remove compile-time calls to proof-ready-for-assistant

Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.
---
 hol-light/hol-light-autotest.el | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'hol-light')

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)
 
-- 
cgit v1.2.3