From 173e6c25b2937d6e6941973aa7b116e1d6405513 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@lilo.org>
Date: Tue, 2 Nov 2021 10:10:34 +0100
Subject: Porting the BTL non-trap loads approach to RTL

---
 backend/RTLgenproof.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'backend/RTLgenproof.v')

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index d07dc968..59d0a451 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -586,9 +586,9 @@ Proof.
   exists (rs1#rd <- v'); exists tm1.
 (* Exec *)
   split. eapply star_right. eexact EX1. eapply exec_Iload. eauto.
-  instantiate (1 := vaddr'). rewrite <- H3.
+  econstructor; eauto. rewrite <- H3.
   apply eval_addressing_preserved. exact symbols_preserved.
-  auto. traceEq.
+  auto.
 (* Match-env *)
   split. eauto with rtlg.
 (* Result *)
-- 
cgit