diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2012-06-03 09:46:07 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2012-06-03 09:46:07 +0000 |
commit | 21ee11059cb76f7f1932616c5a753f93a1bb889d (patch) | |
tree | 3a7557d57cdb434e72d764b894b983264e82fde4 /coq | |
parent | d248f8dfe716749c98143c9bb33dc28e79196d5f (diff) |
Fix a bug of indentation.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 3 | ||||
-rw-r--r-- | coq/ex/indent.v | 9 |
2 files changed, 8 insertions, 4 deletions
@@ -367,7 +367,8 @@ Lemma foo: forall n, ("{" exps "}") ("[" expssss "]") (exp "->" exp) - (exp ":" exp)) + (exp ":" exp) + (exp ".-selector" 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) diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 752bc4f9..28a56515 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -170,11 +170,14 @@ Module X. {auto. } } Qed. - - + + Lemma l2 : forall r:rec, - exists r':rec,r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1). + exists r':rec,r'.(fld1) + = r.(fld2) + /\ r'.(fld2) + = r.(fld1). Proof. intros r. {{ |