diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-07 09:03:11 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-07 09:03:11 +0000 |
| commit | 22e1d84ed757f31c56360da1e01159e764245fb1 (patch) | |
| tree | a05892faa66c7844ec000918a5fbc265dbe531f3 /coq/coq-db.el | |
| parent | fb2383907f7634c96a737e297874f155638d4895 (diff) | |
Require cl for compilation. Rearrange docs.
Diffstat (limited to 'coq/coq-db.el')
| -rw-r--r-- | coq/coq-db.el | 13 |
1 files changed, 6 insertions, 7 deletions
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 <courtieu@lri.fr> ;; 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) |