Commit 6e1db8ce authored by Ralf Jung's avatar Ralf Jung
Browse files

WIP: update for Coq 8.7

parent 64ec23fe
......@@ -118,7 +118,16 @@ Section proof.
wp_let. wp_bind (! _)%E.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
iModIntro. wp_let. wp_bind (ref _)%E.
(* This works. *)
eapply tac_wp_alloc with _ "Hl" _.
let e' := match goal with |- to_val ?e' = _ => e' end in
Undo. Undo.
(* But this does not. *)
wp_alloc l as "Hl".
wp_bind (CAS _ _ _)%E.
iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
destruct (decide (hd = hd')) as [->|Hneq].
Supports Markdown
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