compile warning corrections

2 files changed, 21 insertions, 22 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index c47e2afa..ab8f533d 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -132,16 +132,18 @@
   (if (or (not (char-after)) (char-equal (char-after) ?\n)) t nil)
 )
 
-(defun find-reg (limit reg)
-  (if (< limit (point))
-      (let (x limit) (setq limit (point)) (goto-char x)))
-  (let ((pos nil))
-    (while 
-        (and (not pos)
-             (setq pos (proof-string-match reg (buffer-substring (point) limit))))
-      (forward-char pos)
-      (if (proof-looking-at-syntactic-context) (setq pos nil)))
-    pos)
+(defun find-reg (lim reg)
+  (let ((limit lim))
+	 (if (< limit (point)) ;swap limit and point
+		  (let ((x limit)) (setq limit (point)) (goto-char x)))
+	 (let ((pos nil))
+		(while 
+			 (and (not pos)
+					(setq pos (proof-string-match reg (buffer-substring (point) limit))))
+		  (forward-char pos)
+		  (if (proof-looking-at-syntactic-context) (setq pos nil)))
+		pos)
+	 )
   )
 
 (defun coq-back-to-indentation-prevline ()
@@ -290,7 +292,7 @@
 (defun coq-end-offset (&optional limit)
   "Find the first unclosed open indent item, and returns its column. Stop when reaching limit (defaults tp point-min)"
   (save-excursion
-    (let ((found nil) (cpt 0) (found nil) 
+    (let ((found nil) 
           (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp)))
       (while 
           (and (not found)
@@ -363,9 +365,7 @@
 (defun coq-indent-expr-offset (kind prevcol prevpoint record)
   "Returns the indentation column of the current line. This function indents a *expression* line (a line inside of a command). Use `coq-indent-command-offset' to indent a line belonging to a command. The fourth argument must be t if inside the {}s of a record, nil otherwise."
 
-  (let ((pt (point)) real-start unclosed)
-	 (save-excursion
-		(setq unclosed (coq-find-unclosed 1 prevpoint)))
+  (let ((pt (point)) real-start)
 	 (save-excursion 
 		(setq real-start (coq-find-real-start)))
   
@@ -473,7 +473,7 @@
 
 
 (defun coq-indent-offset ()
-  (let ((col (current-column)) kind prevpt prevcol)
+  (let (kind prevcol prevpoint)
 	 (save-excursion
 		(setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert)
 				prevcol (current-column)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 3ded2e64..06b5897a 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -82,12 +82,11 @@ version of coq by doing 'coqtop -v'."  )
 		(setq coq-version-is-V74 nil) 
 		(setq coq-version-is-V7 nil))
 	  (t 
-		(let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
-				 ;; da: next line not used? Pierre: yes, string-match 1 ... 
-				 ;; at following line returns the last matched regexp (first parenth) 
-				 ;; so we need to make the string-match, and then match-string
-				 (x (string-match "version \\([.0-9]*\\)" str))
-				 (num (match-string 1 str)))
+		(let ((str (shell-command-to-string 
+						(concat coq-prog-name " -v"))))
+		  ;; this match sets match-string below
+		  (string-match "version \\([.0-9]*\\)" str)
+		  (let ((num (match-string 1 str)))
 		  ;; da: added this to avoid type error in case coq command fails
 		  (if (null num) (setq num ""))
 		  (cond
@@ -107,7 +106,7 @@ version of coq by doing 'coqtop -v'."  )
 			 (message v8) 
 			 (setq coq-version-is-V8 t)
 			 (setq coq-version-is-V7 t) 
-			 (setq coq-version-is-V74 t))))))))
+			 (setq coq-version-is-V74 t)))))))))
 
 ;; ----- keywords for font-lock.