diff options
Diffstat (limited to 'mppa_k1c/lib/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index e8835a82..a8da1cf1 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -953,19 +953,17 @@ Proof. - (* PLoadQRRO *) unfold parexec_load_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (ireg_eq _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. + inv H1. Simpl. - (* PLoadORRO *) unfold parexec_load_o_offset in H1. destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - destruct (orb _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. + inv H1. Simpl. - (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. |