From 0a13bf127bb385df424bd9e392742d4fc5bef86a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 13:15:53 +0100
Subject: begin implementing -fcse3-conditions

---
 backend/CSE3analysisproof.v | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

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.
   
   (*
-- 
cgit