Commit 2b52b152 authored by Ralf Jung's avatar Ralf Jung

adjust for heap_adequacy fallout

parent 36f30c73
......@@ -62,7 +62,7 @@ Section ClosedProofs.
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
Proof. apply (heap_adequacy Σ)=> ?. iIntros "_". iApply client_safe. Qed.
End ClosedProofs.
......
......@@ -8,7 +8,7 @@ Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
destruct (Hty _) as [A He]. iStartProof. iDestruct (He $! ) as "#He".
destruct (Hty _) as [A He]. iIntros "_". iDestruct (He $! ) as "#He".
iSpecialize ("He" with "[]"); first by rewrite /env_ltyped.
rewrite subst_map_empty. iApply (wp_wand with "He"); auto.
Qed.
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