diff options
| -rw-r--r-- | aarch64/Asmgenproof.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index db6548fe..7862e9a6 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1587,8 +1587,7 @@ Proof. destruct (peq _ _); try intuition congruence. Qed. -Lemma label_pos_preserved b f lbl z tf: forall - (FIND: Genv.find_funct_ptr ge b = Some (Internal f)) +Lemma label_pos_preserved f lbl z tf: forall (FINDF: transf_function f = OK tf), label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf). Proof. |