From 75e50f13fc3f99aad111b3d83b9919974f8bd58a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 02:40:56 +0100
Subject: [PATCH] CMRAs with identity element are inhabited.

---
 algebra/cmra.v       | 1 +
 program_logic/auth.v | 4 ----
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index bfc450a97..25cbad96f 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -128,6 +128,7 @@ Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
   cmra_empty_left_id :> LeftId (≡) ∅ (⋅);
   cmra_empty_timeless :> Timeless ∅
 }.
+Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅.
 
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
diff --git a/program_logic/auth.v b/program_logic/auth.v
index d5f62fbc4..5f7ce0fbb 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -16,10 +16,6 @@ Section auth.
   Hypothesis auth_valid :
     forall a b, (✓ (Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
 
-  (* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
-  Local Instance auth_inhabited : Inhabited A.
-  Proof. split. exact ∅. Qed.
-
   Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
     (∃ a, own AuthI γ (● a) ★ φ a)%I.
   Definition auth_own (γ : gname) (a : A) : iProp Λ (globalC Σ) := own AuthI γ (◯ a).
-- 
GitLab