diff options
Diffstat (limited to 'backend/Allocation.v')
| -rw-r--r-- | backend/Allocation.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index cf62295d..13e14530 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -36,7 +36,7 @@ Require Import Op Registers RTL Locations Conventions RTLtyping LTL. - a [Lbranch s] instruction. The [block_shape] type below describes all possible cases of structural - maching between an RTL instruction and an LTL basic block. + matching between an RTL instruction and an LTL basic block. *) Inductive move: Type := |