From da32340a8c063c9dc0847d01e7ec5c77ce75f3b1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 09:29:46 +0200 Subject: rm Ofslow --- mppa_k1c/lib/Asmblockgenproof0.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mppa_k1c/lib') diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 0465618c..3bca6629 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -953,7 +953,7 @@ Proof. - (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (eval_offset _ _) in H1; try discriminate. + unfold eval_offset in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. inv H1. Simpl. reflexivity. -- cgit