aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/x-symbol-coq.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-24 23:56:45 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-24 23:56:45 +0000
commitbf211c52fd8fa79c8733fdaf1a127564c33a9829 (patch)
treede70dfa9cbb72c6d7381a70d74de8056e88e6e11 /coq/x-symbol-coq.el
parent92508191870320f68a714d0d1cb8282d3179a8af (diff)
Remove use of proof-ass
Diffstat (limited to 'coq/x-symbol-coq.el')
-rw-r--r--coq/x-symbol-coq.el5
1 files changed, 3 insertions, 2 deletions
diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el
index 44bb4925..c9abbcc8 100644
--- a/coq/x-symbol-coq.el
+++ b/coq/x-symbol-coq.el
@@ -13,6 +13,7 @@
;;
(eval-when-compile
+ (require 'proof-utils) ; to properly compile 'proof-ass'
(require 'cl)) ; to properly compile 'block'
(defvar x-symbol-coq-required-fonts nil)
@@ -162,7 +163,7 @@ or subscript tag."
)))))
(defun coq-match-subscript (limit)
- (if (proof-ass x-symbol-enable)
+ (if coq-x-symbol-enable
(setq x-symbol-coq-subscript-type
(funcall x-symbol-coq-subscript-matcher limit))))
@@ -475,7 +476,7 @@ and `x-symbol-coq-xsymbol-table'."
x-symbol-coq-xsymbol-table)))
(defcustom x-symbol-coq-auto-style
- '((proof-ass x-symbol-enable) ; MODE-ON: whether to turn on interactively
+ '(coq-x-symbol-enable ; MODE-ON: whether to turn on interactively
nil ;; x-symbol-coding
'null ;; x-symbol-8bits [NEVER want it; null disables search]
nil ;; x-symbol-unique