Commit 6b759b62 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove spurious space.

parent dba364cf
......@@ -78,7 +78,7 @@ Section inv.
rewrite assoc_L -!union_difference_L //; set_solver.
Qed.
Lemma own_inv_to_inv M P: own_inv M P - inv M P.
Lemma own_inv_to_inv M P: own_inv M P - inv M P.
Proof.
iIntros "#I". rewrite inv_eq. iIntros (E H).
iPoseProof (own_inv_acc with "I") as "H"; eauto.
......
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