From 24be0361643d8bc2983a17cc47127b9ea2f8a0f2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Aug 2016 18:49:27 +0200
Subject: [PATCH] get rid of a fixed TODO

---
 heap_lang/lib/spawn.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 757d89d5e..ce437f6ca 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -53,7 +53,6 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn /=.
-  (* TODO: Coq is printing %V here.  *)
   wp_let. wp_alloc l as "Hl". wp_let.
   iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
-- 
GitLab