From 3d730bd7c3b25afdcc4a14ddc7c79b9c8ec37fd3 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 7 Jun 2012 15:24:59 +0000 Subject: Fix a bug of indentation in presence of comment. Probably due to a bad set of rules. Fixed by cleaning rules. --- coq/coq.el | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index f6522a2f..05fd9cb6 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -701,7 +701,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((and (equal token ";") (smie-rule-parent-p "." "[" "]" "BeginSubproof" "EndSubproof" "|")) 2) - ((member token '(":=")) 0) + ;((member token '(":=")) 0) ((and (equal token ",") (not (smie-rule-parent-p "forall" "quantif exists"))) 0))) (:before @@ -715,16 +715,17 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (if (smie-rule-prev-p "with match") (- (funcall smie-rules-function :after "with match") 2) (smie-rule-separator kind))) - ((and (equal token ":=") - (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive" - "Function" "Let" "Record" "Instance" "Class" - "Ltac" "Add" "Theorem")) - 2) ;(or proof-indent smie-indent-basic) +; ((and (equal token ":=") +; (smie-rule-parent-p "Definition" "Lemma" "Fixpoint" "Inductive" +; "Function" "Let" "Record" "Instance" "Class" +; "Ltac" "Add" "Theorem")) +; (message ":= FOUND") +; 0) ;(or proof-indent smie-indent-basic) ((and (equal token ":") (smie-rule-parent-p "Definition" "Lemma" "Theorem" "Fixpoint" "Inductive" "Function" "Let" "Record" "Instance" "Class" "Ltac" "Add")) - 2) + 2) ((equal token ".") (if (smie-rule-parent-p "BeginSubproof" "Module" "Section" "Proof") 2)) ((and (equal token "Proof End") -- cgit v1.2.3