diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2012-06-04 11:47:53 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2012-06-04 11:47:53 +0000 |
commit | edfa54e4309400047be6ab3550b12b749baa0caa (patch) | |
tree | 861e3f30766dbd580cec57db3c33bd5651fa212f | |
parent | 8162eb2c09447674c4a0c3ab87b71a675a5261af (diff) |
Fixing indentation (same bug than 2 previous commits). this time it seems ok.
-rw-r--r-- | coq/coq.el | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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" |