From c875003382b2741557d6657ab4611a4c4fa8e9c6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 14 Mar 2020 08:05:37 +0100
Subject: Ireturn

---
 backend/CSE3proof.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 2a33fa1c..a6fc73aa 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -679,8 +679,7 @@ Proof.
          apply WTRS.
     -- econstructor. split.
        + eapply exec_Ireturn; try eassumption.
-         *  erewrite transf_function_at by eauto. simpl.
-         admit.
+         * TR_AT; reflexivity.
          * rewrite stacksize_preserved with (f:=f); eauto.
        + econstructor; eauto.
          simpl. trivial.
-- 
cgit