Commit 946dd99c authored by Robbert Krebbers's avatar Robbert Krebbers

Avoid having FG_increment unfolded in the IH of the counter proof.

TODO: Need to do the same for the stack proof.
TODO: Unfolding should be automatic.
parent 65393b24
......@@ -139,8 +139,8 @@ Section CG_Counter.
- ({E1,E1;Δ;Γ} fill K ((FG_increment $/ LitV (Loc x)) #()) log t : τ).
Proof.
iIntros "#H".
unfold FG_increment. unlock. simpl.
iLöb as "IH".
rewrite {2}/FG_increment. unlock. simpl.
rel_rec_l.
iPoseProof "H" as "H2". (* lolwhat *)
rel_load_l_atomic.
......@@ -169,6 +169,7 @@ Section CG_Counter.
iDestruct "HQ" as "[HQ _]".
iMod ("HQ" with "[Hx HR]").
{ iExists _; iFrame. }
rewrite /FG_increment. unlock. simpl.
iApply "IH".
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