diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-01 19:58:42 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-01 19:58:42 +0200 |
| commit | d1fe9e79ad19feff22f9e319dfafc36a534d9479 (patch) | |
| tree | d855a9ca03d8958fba4926ee04a849f7895f4c97 /backend/CSE3analysisproof.v | |
| parent | 74901c6df6ceb92da58ef5db2592fc05561dce01 (diff) | |
| parent | cb4ddeeeaca4736c2baceecec0511f8f99f465fc (diff) | |
| download | compcert-kvx-d1fe9e79ad19feff22f9e319dfafc36a534d9479.tar.gz compcert-kvx-d1fe9e79ad19feff22f9e319dfafc36a534d9479.zip | |
Merge remote-tracking branch 'origin/parameterized-cse3' into kvx-work
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 382c9f4c..523b52df 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1350,14 +1350,10 @@ Section SOUNDNESS. Proof. unfold apply_cond. intros. - destruct (Compopts.optim_CSE3_conditions tt). - { - pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. - destruct apply_cond1 eqn:COND1. - { apply apply_cond0_sound; auto. } - exact SOUND1. - } - exact REL. + pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1. + destruct apply_cond1 eqn:COND1. + { apply apply_cond0_sound; auto. } + exact SOUND1. Qed. (* |