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 | |
parent | 623c0ad32146f29707067db2fa9549c6d4515885 (diff) | |
download | compcert-fa152aa3e9266f0049614c90a73aa9657e3c4071.tar.gz compcert-fa152aa3e9266f0049614c90a73aa9657e3c4071.zip |
typo in comment
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@106 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-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 bf41908b..3a0ee131 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. *) |