diff options
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 29d171eb..d53cf604 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1350,10 +1350,14 @@ Section SOUNDNESS. Proof. unfold apply_cond. intros. - 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. + 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. Qed. (* |