diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-17 08:25:02 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-17 08:25:02 +0200 |
| commit | 1674f32a0339a0801489336ec15a2e116ba4f95b (patch) | |
| tree | 120286693d09dcd751a2600ad1dbe34f78345d94 /aarch64 | |
| parent | d3b2c5637600704caf0cf8babbc55a4708b8811f (diff) | |
| download | compcert-kvx-1674f32a0339a0801489336ec15a2e116ba4f95b.tar.gz compcert-kvx-1674f32a0339a0801489336ec15a2e116ba4f95b.zip | |
suggestion of simpler name
Diffstat (limited to 'aarch64')
| -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 -> |