From 91aede9bdfac8176126660ddacae07b31e172248 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Mar 2021 13:55:33 +0100
Subject: [PATCH] fixme
---
iris_heap_lang/proph_erasure.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 704a56c57..985c612ce 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -802,7 +802,7 @@ Proof.
apply nsteps_inv_r in Hstps as [[t3 σ3] [Hstps HÏ]]; simpl in *.
destruct (IHn _ _ Hstps) as (t2'&t2''&σ2'&Hostps&?&?&Hprstps); simplify_eq.
edestruct @erased_step_pure_step_tp as [[? Hint]|Hext]; simplify_eq/=;
- eauto 10; [|done..].
+ first apply HÏ; eauto 10; [].
destruct Hext as (i&ei&t2'&efs&e'&κ&Hi1&Ht2&Hpstp);
simplify_eq/=.
rewrite /erase_tp list_lookup_fmap in Hi1.
--
GitLab