Commit f2e1c371 authored by Hai Dang's avatar Hai Dang
Browse files

Fix build

parent db6938b7
......@@ -1224,7 +1224,7 @@ Proof.
(* store our local observations at an old view *)
iCombine "sbs sx Gs1 SLb0 ELx0" as "THUNK".
iDestruct (view_at_intro_incl with "THUNK sV0")
as (V1) "(sV1 & %LeV0 & sbs' & sx' & Gs1' & SLb0' & ELx0' {THUNK}".
as (V1) "(sV1 & %LeV0 & sbs' & sx' & Gs1' & SLb0' & ELx0') {THUNK}".
wp_lam. wp_op. rewrite shift_0.
(* read base stack pointer *)
......
......@@ -809,8 +809,8 @@ Proof.
iDestruct (StackLocal_upgrade_instance with "SI SL1") as "{SL1} #[Gs1 SL1]".
iDestruct (StackLocal_upgrade_instance with "SI SL2") as "{SL2} #[Gs2 SL2]".
iDestruct (graph_snap_union with "Gs1 Gs2") as "$".
iDestruct "SL1'" as (γ γh) "(SS1 & MT1 & II)".
iDestruct "SL2'" as (γ2 γh2) "(SS2 & MT2 & _)".
iDestruct "SL1" as (γ γh) "(SS1 & MT1 & II)".
iDestruct "SL2" as (γ2 γh2) "(SS2 & MT2 & _)".
iDestruct (meta_agree with "MT1 MT2") as %[<- <-]%pair_inj.
iExists γ, γh. iFrame "MT1 II".
iDestruct "SI" as (γ2 T SC) "[G SL]".
......
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