From 6c0f6040fa26ce86b6f0f94908936910a3676b95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk> Date: Mon, 7 Oct 2024 14:34:55 +0100 Subject: [PATCH] Fix global --- stdpp/gmap.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stdpp/gmap.v b/stdpp/gmap.v index 58ffef0a..ea12bae1 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 : -- GitLab