From 9901ff1cd2d38a05145bf0bf929575b134807ed4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 3 Apr 2020 14:47:20 +0200
Subject: [PATCH] Drop stray space

---
 theories/bi/interface.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 41313692c..3ff2090b4 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -371,7 +371,7 @@ Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed.
 Lemma forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
 Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed.
 Lemma forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. eapply (bi_mixin_forall_elim  bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_forall_elim bi_entails), bi_bi_mixin. Qed.
 
 Lemma exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a.
 Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed.
-- 
GitLab