diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-17 13:13:34 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-17 13:13:34 +0000 |
| commit | fa152aa3e9266f0049614c90a73aa9657e3c4071 (patch) | |
| tree | 864bef4aafdbaec8fa0de7f0730e9ca9beb50fe3 /backend/Lineartyping.v | |
| parent | 623c0ad32146f29707067db2fa9549c6d4515885 (diff) | |
typo in comment
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@106 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index bf41908..3a0ee13 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -97,7 +97,7 @@ Definition function_bounds := (max_over_slots_of_funct outgoing_slot))). (** We show that bounds computed by [function_bounds] are all positive - or null, and moreiver [bound_outgoing] is greater or equal to 6. + or null, and moreover [bound_outgoing] is greater or equal to 6. These properties are used later to reason about the layout of the activation record. *) |