diff --git a/algebra/auth.v b/algebra/auth.v index 8bb244b7310383718401ba2c8202bc1a6d07d9be..cd2a8b3265256d40c5bf989f55954e7291ec182c 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.