aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-db.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-db.el')
-rw-r--r--coq/coq-db.el4
1 files changed, 1 insertions, 3 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 7e59bffb..b01e8018 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -25,8 +25,6 @@
(eval-when-compile (require 'cl-lib)) ;decf
-(require 'proof-config)
-(require 'proof-syntax) ; for proof-ids-to-regexp
(require 'holes)
(defconst coq-syntax-db nil
@@ -162,7 +160,7 @@ regexp. See `coq-syntax-db' for DB structure."
(setq l tl)))
; da: next call is wrong?
; (proof-ids-to-regexp res)))
- (concat "\\_<\\(?:" (proof-regexp-alt-list res) "\\)\\_>")))
+ (concat "\\_<\\(?:" (mapconcat #'identity res "\\|") "\\)\\_>")))
;; Computes the max length of strings in a list