From 3c05b1ae3155f21eff0ec68c9ed84c853e55b624 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 4 May 2020 11:48:50 +0200
Subject: [PATCH] a tiny clean up

---
 theories/experimental/helping/helping_stack.v | 2 +-
 theories/logic/proofmode/spec_tactics.v       | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 0ebaadb..8b43ac1 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -343,7 +343,7 @@ Section refinement.
   (* First the case where no offers is accepted *)
   Lemma pop_no_helping_refinement A γo st st' mb lk :
     inv stackN (stackInv A γo st st' mb lk) -∗
-    â–¡ (REL pop_st #st #mb
+    (REL pop_st #st #mb
        <<
       CG_locked_pop (#st', lk)%V : () + A) -∗
     REL pop_st_no_offer #st #mb pop_st
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 98f12b4..4635215 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -539,6 +539,7 @@ Lemma tac_tp_alloc `{relocG Σ} j Δ1 E1 i1 i2 p K' e e' v Q :
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
   e = fill K' (ref e') →
   IntoVal e' v →
+  (* TODO use match here as well *)
   (∀ l : loc, ∃ Δ2,
     envs_simple_replace i2 false
        (Esnoc Enil i2 (j ⤇ fill K' #l)) Δ1 = Some Δ2 ∧
-- 
GitLab