From 569a32b730608002dbb01088660ecf5bfa19dc02 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 27 Jan 2020 17:55:14 +0100
Subject: oper1_sound

---
 backend/CSE2.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 61abbcdf..87460f90 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -499,7 +499,16 @@ Proof.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
-    replace (
+    rewrite args_replace_dst by auto.
+    assumption.
+  }
+  rewrite Regmap.gso by congruence.
+  unfold sem_reg.
+  rewrite PTree.gso by congruence.
+  rewrite Regmap.gso in KILL by congruence.
+  exact KILL.
+Qed.
+
 (*
 Definition apply_instr instr x :=
   match instr with
-- 
cgit