From 233aa0fa650d2e6357baeacf154bbff9c6a4964c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 29 Sep 2016 13:47:53 +0200
Subject: [PATCH] Prove that the auth fragment is a UCMRA homomorphism.

---
 algebra/auth.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index 8bb244b73..cd2a8b326 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -191,7 +191,7 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
-Global Instance auth_frag_cmra_homomorphism : CMRAHomomorphism (Auth None).
+Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
 Proof. done. Qed.
 
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
-- 
GitLab