From 1e512d6e86ead660a5fd64299792bc29c1885016 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 6 Apr 2020 13:03:09 +0200 Subject: [PATCH] use type-ascribed equality notation --- theories/algebra/gmap.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index a94bce9f..098a55eb 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -285,18 +285,18 @@ Proof. Qed. Lemma core_singleton (i : K) (x : A) cx : - pcore x = Some cx → core ({[ i := x ]} : gmap K A) = {[ i := cx ]}. + pcore x = Some cx → core {[ i := x ]} =@{gmap K A} {[ i := cx ]}. Proof. apply omap_singleton. Qed. Lemma core_singleton' (i : K) (x : A) cx : - pcore x ≡ Some cx → core ({[ i := x ]} : gmap K A) ≡ {[ i := cx ]}. + pcore x ≡ Some cx → core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}. Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx'). Qed. Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) : - core ({[ i := x ]} : gmap K A) = {[ i := core x ]}. + core {[ i := x ]} =@{gmap K A} {[ i := core x ]}. Proof. apply core_singleton. rewrite cmra_pcore_core //. Qed. Lemma op_singleton (i : K) (x y : A) : - {[ i := x ]} ⋅ {[ i := y ]} = ({[ i := x ⋅ y ]} : gmap K A). + {[ i := x ]} ⋅ {[ i := y ]} =@{gmap K A} {[ i := x ⋅ y ]}. Proof. by apply (merge_singleton _ _ _ x y). Qed. Global Instance is_op_singleton i a a1 a2 : IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}. -- GitLab