diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2013-07-11 14:58:35 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2013-07-11 14:58:35 +0000 |
| commit | 5cd9adb60e8b6e5fd1ce87adcf263c3a8b358cdc (patch) | |
| tree | 69975a43fcce6d33d0e2cd40ebf0ac03a79cbecb /coq/ex | |
| parent | 2ee032846aa8e985478055f3b3b289439fb5860a (diff) | |
Fixing another bug in indentation concerning "where". Actually there
are other uses of "where (declaring notation for records that I did no
test).
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 34286fed..c574f715 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -172,10 +172,11 @@ Class cla {X:Set}:Set := { Module X. - Lemma l : - forall r:rec, - exists r':rec, - r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1). + Lemma l + : + forall r:rec, + exists r':rec, + r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1). Proof. intros r. { exists |