diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 6cf5d9404f92739bcdd700deb23e98cfb2b2a597..4e2e529bc07709c77037d52c0b9bb048522ec746 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -63,6 +63,13 @@ Section definitions.
     let (X) := X in dom X.
 End definitions.
 
+Section more_definitions.
+  Context `{Countable A} `{Countable B}.
+
+  Definition gmultiset_map f (X : gmultiset A) : gmultiset B :=
+    list_to_set_disj (f <$> elements X).
+End more_definitions.
+
 Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
 Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
 Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
@@ -783,9 +790,6 @@ Section map.
 
   Implicit Type f : A → B.
 
-  Definition gmultiset_map f (X : gmultiset A) : gmultiset B :=
-    list_to_set_disj (f <$> elements X).
-
   Lemma elem_of_gmultiset_map f X y :
     y ∈ gmultiset_map f X ↔ ∃ x, y = f x ∧ x ∈ X.
   Proof.