diff options
author | Makarius Wenzel <makarius@sketis.net> | 1999-11-10 14:20:00 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 1999-11-10 14:20:00 +0000 |
commit | 8423337a5cf175abcb3f9cca77ed49b3b79e1caa (patch) | |
tree | 726f90aaaab92ca2396b72ffa87a5fc1ae33bb00 /coq | |
parent | 24c86f6ce52b633973e12457c6ec8c7133209dc7 (diff) |
fixed indentation bug: use proof-looking-at (proof-case-fold-search);
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -343,7 +343,7 @@ (save-excursion (move-to-column (current-indentation)) (cond ((eq (char-after (point)) ?|) (+ col 3)) - ((looking-at "end") col) + ((proof-looking-at "end") col) (t (+ col 5))))) ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)) (+ col (if (eq ?| (save-excursion @@ -354,16 +354,16 @@ (defun coq-parse-indent (c stack) (cond ((eq c ?C) - (cond ((looking-at "Case") + (cond ((proof-looking-at "Case") (cons (list ?c (point)) stack)) - ((looking-at "CoInductive") + ((proof-looking-at "CoInductive") (forward-char (length "CoInductive")) (cons (list c (- (point) (length "CoInductive"))) stack)) (t stack))) - ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c)) + ((and (eq c ?e) (proof-looking-at "end") (eq (car (car stack)) ?c)) (cdr stack)) - ((and (eq c ?I) (looking-at "Inductive")) + ((and (eq c ?I) (proof-looking-at "Inductive")) (forward-char (length "Inductive")) (cons (list c (- (point) (length "Inductive"))) stack)) |