diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 342b98d0..7f30eddf 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -90,7 +90,7 @@ Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := i = control_to_instruction cfi -> is_nth_inst bb n i. -Lemma find_bblock_find_instr_correct pos n lb tlb bb: +Lemma find_instr_bblock pos n lb tlb bb: find_bblock pos lb = Some bb -> unfold lb = OK tlb -> 0 <= n < size bb -> |