Commit c7f5f4cc authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of more scopes.

parent 946dd99c
......@@ -24,9 +24,9 @@ Section Stack_refinement.
Lemma FG_CG_push_refinement st st' (τi : D) (v v' : val) l {τP : ww, PersistentP (τi ww)} Γ :
inv stackN (sinv τi st st' l) - τi (v,v') -
Γ ((FG_push $/ (LitV (Loc st))) v)%E log ((CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v')%E : TUnit.
Γ (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
Proof.
iIntros "#Hinv #Hvv'". iIntros (Δ).
iIntros "#Hinv #Hvv'" (Δ).
Transparent FG_push.
unfold CG_locked_push. unlock. simpl_subst/=.
rel_rec_r.
......
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