diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:29:46 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:29:46 +0200 |
| commit | da32340a8c063c9dc0847d01e7ec5c77ce75f3b1 (patch) | |
| tree | 4eb8730dc8a6703d048955865d6cb630eb6b859f /mppa_k1c/lib | |
| parent | 981adc51dd17dbb97572e7c27423628b5c9eada4 (diff) | |
| download | compcert-kvx-da32340a8c063c9dc0847d01e7ec5c77ce75f3b1.tar.gz compcert-kvx-da32340a8c063c9dc0847d01e7ec5c77ce75f3b1.zip | |
rm Ofslow
Diffstat (limited to 'mppa_k1c/lib')
| -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. |