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

remove some spurious spaces

parent 9e1582b9
No related branches found
No related tags found
No related merge requests found
......@@ -60,7 +60,7 @@ Proof.
- rewrite uPred_fupd_unseal. solve_proper.
- intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
by iIntros "($ & $ & HE) !> !> [$ $] !> !>" .
by iIntros "($ & $ & HE) !> !> [$ $] !> !>".
- rewrite uPred_fupd_unseal.
iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
- rewrite uPred_fupd_unseal.
......@@ -142,7 +142,7 @@ Proof.
(* We don't actually want any credits, but we need the [lcGS]. *)
iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hc]".
set (Hi := InvG HasNoLc _ Hw Hc).
iAssert (|={,E2}=> P)%I with "[Hc]" as "H" .
iAssert (|={,E2}=> P)%I with "[Hc]" as "H".
{ iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd; last done. }
rewrite uPred_fupd_unseal /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
......
......@@ -62,4 +62,4 @@ Global Instance pretty_bin_op : Pretty bin_op :=
| LtOp => "<"
| EqOp => "="
| OffsetOp => "+ₗ"
end .
end.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment