From 3570acccb66403ca2c2fb2fd00042534bcb7abc9 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 18 Dec 2017 18:00:30 +0100
Subject: [PATCH] Add Inhabited in bi_index.

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

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0f7a3ea09..674c27231 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -5,10 +5,11 @@ From iris.bi Require Import derived_laws.
 Structure bi_index :=
   BiIndex
     { bi_index_type :> Type;
+      bi_index_inhabited : Inhabited bi_index_type;
       bi_index_rel : SqSubsetEq bi_index_type;
       bi_index_rel_preorder : PreOrder (⊑) }.
 
-Existing Instances bi_index_rel bi_index_rel_preorder.
+Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
 
 Section Ofe_Cofe.
 Context {I : bi_index} {PROP : bi}.
@@ -483,9 +484,9 @@ Proof.
   by apply absorbing, bi.forall_absorbing.
 Qed.
 Global Instance monPred_all_affine P :
-  Inhabited I → Affine P → Affine (@monPred_all I PROP P).
+  Affine P → Affine (@monPred_all I PROP P).
 Proof.
-  move=>? []. unfold Affine. unseal=>Hp. split => ?.
+  move=> []. unfold Affine. unseal=>Hp. split => ?.
   by apply affine, bi.forall_affine.
 Qed.
 End bi_facts.
-- 
GitLab