From 22e1d84ed757f31c56360da1e01159e764245fb1 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 7 Sep 2009 09:03:11 +0000 Subject: Require cl for compilation. Rearrange docs. --- coq/coq-db.el | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'coq/coq-db.el') diff --git a/coq/coq-db.el b/coq/coq-db.el index 1be7719a..c063b6dd 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -3,19 +3,18 @@ ;; Author: Pierre Courtieu ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; - -;;; We store all information on keywords (tactics or command) in big +;; +;;; Commentary: +;; +;; We store all information on keywords (tactics or command) in big ;; tables (ex: `coq-tactics-db') From there we get: menus including ;; "smart" commands, completions for command coq-insert-... -;; abbrev tables and font-lock keyword - -;;; real value defined below - -;;; Commentary: +;; abbrev tables and font-lock keyword. ;; ;;; Code: +(require 'cl) (require 'proof-config) ; for proof-face-specs, a macro (require 'holes) -- cgit v1.2.3