diff --git a/iris/algebra/view.v b/iris/algebra/view.v index aa39cebce3343c2038caedbea0024df4f06b7b50..cca42710d54a736697a52000892c7434ef9d8608 100644 --- a/iris/algebra/view.v +++ b/iris/algebra/view.v @@ -216,7 +216,8 @@ Section cmra. core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x)) := eq_refl _. Local Definition view_op_eq : - op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y) (view_frag_proj x ⋅ view_frag_proj y) + op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y) + (view_frag_proj x ⋅ view_frag_proj y) := eq_refl _. Lemma view_cmra_mixin : CmraMixin (view rel).