From fd7485fb5dbff2e598fe46aece9829c7dfe0ec62 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 19 Oct 2020 16:31:54 +0200 Subject: Typo in label_pos_preserved hyp --- aarch64/Asmgenproof.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'aarch64/Asmgenproof.v') 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. -- cgit