Skip to content
Snippets Groups Projects
Commit 7746448f authored by Ralf Jung's avatar Ralf Jung
Browse files

prepare for weaker f_equiv

parent 56183e18
No related branches found
No related tags found
No related merge requests found
Pipeline #54462 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/ghostcell.v
+ 2
− 2
View file @ 7746448f
......@@ -101,8 +101,8 @@ Section ghostcell.
Proof.
rewrite /Fractional=>q1 q2.
rewrite -own_op /ghosttoken_st_to_R /=. f_equiv.
rewrite -Cinr_op. f_equiv.
rewrite -pair_op. f_equiv.
rewrite -Cinr_op. eapply Cinr_proper.
rewrite -pair_op. f_equiv; [|done..].
rewrite agree_idemp. done.
Qed.
......
theories/typing/own.v
+ 1
− 1
View file @ 7746448f
......@@ -39,7 +39,7 @@ Section own.
- iSplit.
+ by iIntros "[[]?]".
+ by iIntros "[]".
- rewrite heap_freeable_op_eq. f_equiv.
- rewrite heap_freeable_op_eq. f_equiv; [|done..].
by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
Qed.
......
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