aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2012-06-04 11:47:53 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2012-06-04 11:47:53 +0000
commitedfa54e4309400047be6ab3550b12b749baa0caa (patch)
tree861e3f30766dbd580cec57db3c33bd5651fa212f
parent8162eb2c09447674c4a0c3ab87b71a675a5261af (diff)
Fixing indentation (same bug than 2 previous commits). this time it seems ok.
-rw-r--r--coq/coq.el4
1 files 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"