From c230e600adeb35f4c174c68812712cf50a45fe44 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 14 Apr 2004 15:53:53 +0000
Subject: added basic support for imenu for coq.

---
 coq/coq-syntax.el | 6 ++++++
 coq/coq.el        | 4 +++-
 2 files changed, 9 insertions(+), 1 deletion(-)

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)
diff --git a/coq/coq.el b/coq/coq.el
index b6e104c1..d664d2b3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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
-- 
cgit v1.2.3