diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 0ebaadb0a5f5c09d1c86de52742dba677859c861..8b43ac1ddb0eaa3a4383cd94711cf30b1351ef49 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 98f12b48e4728962289ca8d10640b7a92047f249..4635215d88256c8b18cfcfcaa6363fdf7ea9d434 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 ∧