From ac2ed5ec6a3fee36abd1ca0aca2f049c1ce0fb01 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 25 Aug 2006 13:21:20 +0000
Subject: Adding comments

---
 coq/coq-syntax.el | 17 ++++++++++++++---
 coq/coq.el        |  2 ++
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 2775ac2d..0c96a79b 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -823,10 +823,21 @@ Used by `coq-goal-command-p'"
 ;(defconst coq-with-with-hole-regexp
 ;  (concat "\\(" "with" "\\)\\s-+\\(" coq-ids "\\)" "\\(?:[^:]+\\|:[^=]\\)*:="))
 
+; must match:
+; with f :=
+; with f : foo :=
+; with f x y :=
+; with f x y : t :=
+; with f (x:tx) y :=
+; with f (x:tx) (y:ty) :=
+; BUT NOT:
+; with f ...(x:=t)...
+; the simplest is : 
+; either no '(' before the first ':' 
+;     OR the first := found follows a ')[^(.]*'
+; actually this wont colorize f in 'with f (x:t) : foo.bar :="' but that is acceptable
 (defconst coq-with-with-hole-regexp
-  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(]*:\\|.*)[^(.]*:=\\)")
-  ;(concat "\\(" "with" "\\)\\s-+\\(" coq-id "\\)" ".*?)[^(.]*:=")
-  )
+  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(]*:\\|.*)[^(.]*:=\\)"))
 
 (defvar coq-font-lock-keywords-1
    (append
diff --git a/coq/coq.el b/coq/coq.el
index b0e3e2fb..55406a81 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -164,6 +164,7 @@ To disable coqc being called (and use only make), set this to nil."
 (defvar coq-non-retractable-instruct-regexp 
   (proof-ids-to-regexp coq-non-retractable-instruct))
 
+; delete when no more support for 8.0 ?
 (defvar coq-keywords-section
   '("Section" "Module\\s-+Type" "Declare\\s-+Module" "Module"))
 
@@ -264,6 +265,7 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
 ; if no second id --> name of the module/section is (match-string 2 str)
 ; otherwise it is (match-string 5 str) 
 ; to know if there is a second id: (match-string 2 str)="Type" ?
+; delete when no more support for 8.0
 (defun coq-section-or-module-start-p (str)
   (proof-string-match 
    (concat "\\`" coq-section-regexp 
-- 
cgit v1.2.3