From 763c157a214f46ef80c92c4eeafb2d705bedbde7 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Wed, 3 Jun 1998 14:00:53 +0000
Subject: Changed expression (>= 0 x) to its equivalent (eq x 0) Changed some
 variables to their associated constant in cases where we know they must be
 equal.

---
 proof-indent.el | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/proof-indent.el b/proof-indent.el
index d4c5e577..42a2542b 100644
--- a/proof-indent.el
+++ b/proof-indent.el
@@ -48,19 +48,20 @@
 	  (if (eq c ?\") (setq instring nil)))
 	 (t (cond
 	     ((eq c ?\()
-	      (if (looking-at "(\\*") (progn 
-					(incf comment-level)
-					(forward-char))
-		;; Why is this >= 0?  Surely it's always true!
-		(if (>= 0 comment-level) 
-		    (setq stack (cons (list c (point)) stack)))))
+	      (cond
+	       ((looking-at "(\\*")
+		(progn
+		  (incf comment-level)
+		  (forward-char)))
+	       ((eq comment-level 0)
+		(setq stack (cons (list ?\( (point)) stack)))))
 	     ((and (eq c ?\*) (looking-at "\\*)"))
 	      (decf comment-level)
 	      (forward-char))
 	     ((> comment-level 0))
 	     ((eq c ?\") (setq instring t))
 	     ((eq c ?\[)
-	      (setq stack (cons (list c (point)) stack)))
+	      (setq stack (cons (list ?\[ (point)) stack)))
 	     ((or (eq c ?\)) (eq c ?\]))
 	      (setq stack (cdr stack)))
 	     ((looking-at proof-commands-regexp)
-- 
cgit v1.2.3