From edae2dc190b43ef493432ecf578dc426e45fda9a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 4 Dec 2017 19:04:57 +0100
Subject: [PATCH] Lemma -> Global Instance.

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

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 4c03ecd64..f8a5aea4c 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -610,7 +610,7 @@ Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_pro
 
 (** PlainlyExist1BI *)
 
-Lemma uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
+Global Instance uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
 Proof. unfold PlainlyExist1BI. by unseal. Qed.
 
 (** Limits *)
-- 
GitLab