diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2012-06-04 16:07:15 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2012-06-04 16:07:15 +0000 |
| commit | b3af77749ed07f58316371c456e78c8d7aca1505 (patch) | |
| tree | 97c2f96fa926cbadf7a384d96dc9c4eb3dec2c55 /coq/ex | |
| parent | edfa54e4309400047be6ab3550b12b749baa0caa (diff) | |
One more fix for indentation.
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 28a56515..a6fda706 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -174,10 +174,11 @@ Module X. Lemma l2 : forall r:rec, - exists r':rec,r'.(fld1) - = r.(fld2) - /\ r'.(fld2) - = r.(fld1). + exists r':rec, + ressai.(fld1) + = r.(fld2) + /\ r'.(fld2) + = r.(fld1). Proof. intros r. {{ |