diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-10-28 10:45:21 +0200 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-10-28 10:45:21 +0200 |
| commit | 3b621d71274bc62722876c7229c2e649be6cb378 (patch) | |
| tree | 07ccd4de15cd2111a78fecf36c3b56364871725f /coq/coq-syntax.el | |
| parent | 8c5d463e71f4b0966359cded7efb051e8e4487f7 (diff) | |
fix coq-require-command-regexp (fixes #75)
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 195636a5..5aa41292 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,10 +1304,6 @@ It is used: ;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) ;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -;; (defconst coq-require-command-regexp -;; (concat "Require\\s-+\\(" coq-id "\\)") -;; "Regular expression matching Require commands in Coq. -;; Group number 1 matches the name of the library which is required.") (defconst coq-context-marker-regexp (concat (regexp-opt '("ltac" "constr" "uconstr") 'symbols) ":")) |