From edfa54e4309400047be6ab3550b12b749baa0caa Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 4 Jun 2012 11:47:53 +0000 Subject: Fixing indentation (same bug than 2 previous commits). this time it seems ok. --- coq/coq.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 9a3a9ea8..ff243823 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -367,8 +367,7 @@ Lemma foo: forall n, ("{" exps "}") ("[" expssss "]") (exp "->" exp) - (exp ":" exp) - (exp ".-selector" exp)) + (exp ":" exp)) ;; Having "return" here rather than as a separate rule in `exp' causes ;; it to be indented at a different level than "with". (matchexp (matchexp "return" exp) (exp "in" exp)) ;(exp "as" exp) @@ -450,6 +449,7 @@ Lemma foo: forall n, ;; "let x:=3; y:=4 in...". ;; - We distinguish the ".-selector" from the terminator "." for ;; obvious reasons. +;; - We consider qualified.names as one single token for obvious reasons. ;; - We distinguish the "Module M." from "Module M := exp." since the first ;; opens a new scope (closed by End) whereas the other doesn't. ;; - We drop "Program" because it's easier to consider "Program Function" -- cgit v1.2.3