diff --git a/algebra/cmra.v b/algebra/cmra.v index bfc450a974d62555665ff878dbd6389c9e2ad071..25cbad96fb6de565466bd790b6d406cd106d63f3 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 d5f62fbc425229b24511ab696c15e0e5c7ca2301..5f7ce0fbb9725a0131aa15a1be95449f561d0c3b 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).