diff --git a/stdpp/gmap.v b/stdpp/gmap.v index 58ffef0a5d3fe7a8dc95a0a598a23be543d9b544..ea12bae1a2a62e5e89bdb624b262d09f155cb3d6 100644 --- a/stdpp/gmap.v +++ b/stdpp/gmap.v @@ -826,7 +826,7 @@ End gset. Section gset_cprod. Context `{Countable A, Countable B}. - #[global] Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) := + Global Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) := λ X Y, set_bind (λ e1, set_map (e1,.) Y) X. Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :