diff options
| author | Hendrik Tews | 2016-10-28 10:45:21 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2016-10-28 10:45:21 +0200 |
| commit | 3b621d71274bc62722876c7229c2e649be6cb378 (patch) | |
| tree | 07ccd4de15cd2111a78fecf36c3b56364871725f | |
| parent | 8c5d463e71f4b0966359cded7efb051e8e4487f7 (diff) | |
fix coq-require-command-regexp (fixes #75)
| -rw-r--r-- | coq/coq-compile-common.el | 4 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 4 |
2 files changed, 3 insertions, 5 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 8ce4b0c2..5a5b63c9 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -310,7 +310,9 @@ Note that the trailing dot in \"Require A.\" is not part of the module identifier and should therefore not be matched by this regexp.") (defconst coq-require-command-regexp - "\\(?:^From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*\\)?\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*" + (concat "^\\(?:From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)" + "[ \t\n]*\\)?" + "\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*") "Regular expression matching Require commands in Coq. Should match \"Require\" with its import and export variants up to (but not including) the first character of the first required module. The required 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) ":")) |