Commit 24be0361 authored by Ralf Jung's avatar Ralf Jung

get rid of a fixed TODO

parent 6d038c53
...@@ -53,7 +53,6 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) : ...@@ -53,7 +53,6 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
WP spawn e {{ Φ }}. WP spawn e {{ Φ }}.
Proof. Proof.
iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn /=. iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn /=.
(* TODO: Coq is printing %V here. *)
wp_let. wp_alloc l as "Hl". wp_let. wp_let. wp_alloc l as "Hl". wp_let.
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment