diff options
| -rw-r--r-- | coq/coq-syntax.el | 6 | ||||
| -rw-r--r-- | coq/coq.el | 4 |
2 files changed, 9 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 122b9e02..6ff24e4d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -839,6 +839,12 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?\) ")(4")) +(defconst coq-generic-expression + (mapcar (lambda (kw) + (list (capitalize kw) + (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) + 1)) + (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) (provide 'coq-syntax) @@ -614,7 +614,9 @@ This is specific to coq-mode." proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>. proof-save-with-hole-regexp coq-save-with-hole-regexp proof-goal-with-hole-regexp coq-goal-with-hole-regexp - proof-nested-undo-regexp coq-state-changing-commands-regexp) + proof-nested-undo-regexp coq-state-changing-commands-regexp + proof-script-imenu-generic-expression coq-generic-expression + ) (setq ;indentation is implemented in coq-indent.el |