diff options
author | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-02 12:41:30 +0000 |
---|---|---|
committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-02 12:41:30 +0000 |
commit | d6ff63eac2e02856b2031aafb23a75f17256b631 (patch) | |
tree | 11f3a5926ec17a8d7d0aad09cf17679f73ac797b /coq/coq.el | |
parent | c25e3c1a1c3c12a81f90b0a20321ca9734634032 (diff) |
fixed minor bugs
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 14 |
1 files changed, 11 insertions, 3 deletions
@@ -6,16 +6,24 @@ ;; $Id$ -(require 'proof) +(require 'proof-script) (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")) + '(pbp-mode proof-shell-config-done))) ;; FIXME: outline and info should be autoloaded. (require 'outline) (require 'info) ; Configuration -(setq tag-always-exact t) ; Tags is unusable with Coq library otherwise: +(setq tags-always-exact t) ; Tags is unusable with Coq library otherwise: (defcustom coq-tags "/usr/local/lib/coq/theories/TAGS" "the default TAGS table for the Coq library" @@ -414,7 +422,7 @@ proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp proof-shell-init-cmd nil proof-analyse-using-stack t - proof-lift-global coq-lift-global) + proof-lift-global 'coq-lift-global) ;; The following hook is removed once it's called. (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t) |