From 5040ad4de827192f93325a2520a7b7410994c166 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 16 Jul 2000 15:18:47 +0000
Subject: Removed some (hopefully redundant) requires.

---
 coq/coq.el | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 5f711f89..07ceef3e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -5,19 +5,10 @@
 
 ;; $Id$ 
 
-(require 'proof-script)
+(require 'proof)
 (require 'coq-syntax)
 
-;; Spans are our abstraction of extents/overlays.
-(eval-and-compile
-  (cond ((fboundp 'make-extent) (require 'span-extent))
-	((fboundp 'make-overlay) (require 'span-overlay))))
-
-(eval-and-compile
-  (mapcar (lambda (f) (autoload f "proof-shell"))
-	    '(proof-goals-mode proof-shell-config-done))) 
-
-; Configuration
+;; Configuration
 
 (setq tags-always-exact t) ; Tags is unusable with Coq library otherwise:
 
-- 
cgit v1.2.3