From 0758845e2d5d3374efef08fcc27401705b51fe84 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 May 2017 11:35:47 +0200
Subject: [PATCH] Fix another FIXME.
The tactic `iFrame` frames the spatial context in order, it does not do repeat
`iFrame anyHyp`. As a result, when you have evars, things become ambigious
---
theories/typing/lib/mutex/mutex.v | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 2c3f212c..8d86ce50 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -167,9 +167,7 @@ Section code.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
iFrame. iSplitL "Hx".
- iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
- - iExists (_ :: vl). rewrite heap_mapsto_vec_cons. iFrame.
- (* FIXME: Why does calling `iFrame` twice even make a difference? *)
- iFrame. eauto. }
+ - iExists (#false :: vl). rewrite heap_mapsto_vec_cons. iFrame; eauto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
--
GitLab