From e11b548d94b247b5359960b8d31027b53ee0dffc Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 16 Jul 2021 20:47:25 +0200
Subject: rm condition parametrization in CSE3analysis

---
 backend/CSE3analysis.v      |  7 ++-----
 backend/CSE3analysisproof.v | 12 ++++--------
 2 files changed, 6 insertions(+), 13 deletions(-)

(limited to 'backend')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 75e00f67..9a6c9c0d 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -477,13 +477,10 @@ Section OPERATIONS.
     end.
 
   Definition apply_cond cond args (rel : RELATION.t) : RB.t :=
-    if Compopts.optim_CSE3_conditions tt
-    then 
-      match apply_cond1 cond args rel with
+    match apply_cond1 cond args rel with
       | Some rel => Some (apply_cond0 cond args rel)
       | None => RB.bot
-      end
-    else Some rel.
+    end.
       
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) :=
   match instr with
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.
   
   (*
-- 
cgit