diff --git a/algebra/gset.v b/algebra/gset.v index 2d4addaf0ce5fe1dc355591aa2a82f14ed105288..a00ced7855c7601156bbb13823dfc25c0b198639 100644 --- a/algebra/gset.v +++ b/algebra/gset.v @@ -54,7 +54,7 @@ Section gset. intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX. Qed. - Global Instance gmap_persistent X : Persistent X. + Global Instance gset_persistent X : Persistent X. Proof. by apply persistent_total; rewrite gset_core_self. Qed. End gset.