From 6b759b6202c13c4b6bee65dc3aef0b56839810c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:09:21 +0200
Subject: [PATCH] Remove spurious space.

---
 theories/base_logic/lib/invariants.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 790e5e51d..c8e996fa2 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -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.
-- 
GitLab