diff options
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 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. *) |