Commit 0c8495a1 authored by Ralf Jung's avatar Ralf Jung

fix treiber

parent d6222bb0
......@@ -114,7 +114,7 @@ Section proof.
destruct (decide (hd = hd')) as [->|Hneq].
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" with "[-]") as "HQ".
{ by eauto with iFrame. }
{ simpl. by eauto 10 with iFrame. }
iModIntro. wp_if. eauto.
* wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
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