From 33d2208eb0413fdc8845fb070f602601528c5bb1 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 24 Mar 2000 15:28:00 +0000
Subject: Removed spurious requires

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

diff --git a/coq/coq.el b/coq/coq.el
index 014bd8ce..ef6f2c92 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -16,9 +16,6 @@
 (eval-and-compile
   (mapcar (lambda (f) (autoload f "proof-shell"))
 	    '(pbp-mode proof-shell-config-done))) 
-;; FIXME: outline and info should be autoloaded.
-(require 'outline)
-(require 'info)
 
 ; Configuration
 
@@ -271,27 +268,24 @@
 	   (proof-string-match ":=" cmd))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Commands specific to coq                                      ;;
+;;   Commands specific to coq                                       ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun coq-Intros () 
   "Shortcut for Intros.
-
-  This is specific to coq-mode." 
+This is specific to coq-mode." 
   (interactive) 
   (insert "Intros "))
 
 (defun coq-Apply () 
   "Shortcut for Apply
-
-  This is specific to coq-mode."  
+This is specific to coq-mode."  
   (interactive) 
   (insert "Apply "))
 
 (defun coq-SearchIsos ()
   "Search a term whose type is isomorphic to given type
-
-  This is specific to coq-mode."
+This is specific to coq-mode."
   (interactive)
   (let (cmd)
     (proof-shell-ready-prover) 
@@ -506,7 +500,7 @@
    proof-shell-assumption-regexp coq-id
    proof-shell-first-special-char ?\360
    proof-shell-wakeup-char ?\371 ; done: prompt
-					; The next three represent path annotation information
+   ;; The next three represent path annotation information
    proof-shell-start-char ?\372 ; not done
    proof-shell-end-char ?\373 ; not done
    proof-shell-field-char ?\374 ; not done
-- 
cgit v1.2.3