diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |