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/ex | |
| parent | d248f8dfe716749c98143c9bb33dc28e79196d5f (diff) | |
Fix a bug of indentation.
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 9 |
1 files changed, 6 insertions, 3 deletions
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. {{ |