From a1f630a63eda08c92449ff63472a3b1b4bea4946 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 18 Dec 2017 19:44:03 +0100
Subject: [PATCH] Weaken monPred_bi_embedding. A bi index is always inhabited.

---
 theories/bi/monpred.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0c363af6f..daba741fb 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -468,8 +468,7 @@ Proof.
   by apply affine, bi.forall_affine.
 Qed.
 
-Global Instance monPred_bi_embedding :
-  Inhabited I → BiEmbedding PROP (monPredI I PROP).
+Global Instance monPred_bi_embedding : BiEmbedding PROP (monPredI I PROP).
 Proof.
   split; try apply _; unseal; try done.
   - move =>?? /= [/(_ inhabitant) ?] //.
@@ -501,7 +500,6 @@ Proof.
   by apply timeless, bi.forall_timeless.
 Qed.
 
-Global Instance monPred_sbi_embedding :
-  Inhabited I → SbiEmbedding PROP (monPredSI I PROP).
+Global Instance monPred_sbi_embedding : SbiEmbedding PROP (monPredSI I PROP).
 Proof. split; try apply _. by unseal. Qed.
 End sbi_facts.
-- 
GitLab