diff --git a/tests/gmap.ref b/tests/gmap.ref
new file mode 100644
index 0000000000000000000000000000000000000000..a4d42549233b5c0153c1b455eb21f2651d09f7d4
--- /dev/null
+++ b/tests/gmap.ref
@@ -0,0 +1,72 @@
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  {[1; 2; 3]} = ∅
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  elements {[1; 2; 3]} = []
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  {[1; 2; 3]} ∖ {[1]} ∪ {[4]} ∩ {[10]} = ∅ ∖ {[2]}
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  1 ∈ dom (gset nat) (<[1:=2]> ∅)
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ = {[1; 2; 3]}) = false
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ≡ {[1; 2; 3]}) = false
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (1 ∈ {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ## {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
+1 goal
+  
+  ============================
+  bool_decide (∅ ⊆ {[1; 2; 3]}) = true
diff --git a/tests/gmap.v b/tests/gmap.v
new file mode 100644
index 0000000000000000000000000000000000000000..8fdc617474e441e0b5951c6a9a90bf2e7b725711
--- /dev/null
+++ b/tests/gmap.v
@@ -0,0 +1,70 @@
+From stdpp Require Import gmap.
+
+Goal {[1; 2; 3]} =@{gset nat} ∅.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal elements (C := gset nat) {[1; 2; 3]} = [].
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal
+  {[1; 2; 3]} ∖ {[ 1 ]} ∪ {[ 4 ]} ∩ {[ 10 ]} =@{gset nat} ∅ ∖ {[ 2 ]}.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal 1 ∈ dom (M := gmap _ _) (gset _) (<[ 1 := 2 ]> ∅).
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+Abort.
+
+Goal bool_decide (∅ =@{gset _} {[ 1; 2; 3 ]}) = false.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ≡@{gset _} {[ 1; 2; 3 ]}) = false.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (1 ∈@{gset _} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ##@{gset _} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
+
+Goal bool_decide (∅ ⊆@{gset _} {[ 1; 2; 3 ]}) = true.
+Proof.
+  Fail progress simpl.
+  Fail progress cbn.
+  Show.
+  reflexivity.
+Qed.
diff --git a/theories/gmap.v b/theories/gmap.v
index 79813f63de28e77faf5743027aec1d9ffe655f3d..97726848b7b816d38e1ffb547545094017bf71b6 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -237,7 +237,7 @@ Definition gset K `{Countable K} := mapset (gmap K).
 
 Section gset.
   Context `{Countable K}.
-  (* Lift instances of operational TCs from [mapset]. *)
+  (* Lift instances of operational TCs from [mapset] and mark them [simpl never]. *)
   Global Instance gset_elem_of: ElemOf K (gset K) := _.
   Global Instance gset_empty : Empty (gset K) := _.
   Global Instance gset_singleton : Singleton K (gset K) := _.
@@ -253,6 +253,21 @@ Section gset.
   Global Instance gset_subseteq_dec : RelDecision (⊆@{gset K}) := _.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
 
+  Global Arguments gset_elem_of : simpl never.
+  Global Arguments gset_empty : simpl never.
+  Global Arguments gset_singleton : simpl never.
+  Global Arguments gset_union : simpl never.
+  Global Arguments gset_intersection : simpl never.
+  Global Arguments gset_difference : simpl never.
+  Global Arguments gset_elements : simpl never.
+  Global Arguments gset_eq_dec : simpl never.
+  Global Arguments gset_countable : simpl never.
+  Global Arguments gset_equiv_dec : simpl never.
+  Global Arguments gset_elem_of_dec : simpl never.
+  Global Arguments gset_disjoint_dec : simpl never.
+  Global Arguments gset_subseteq_dec : simpl never.
+  Global Arguments gset_dom : simpl never.
+
   (* Lift instances of other TCs. *)
   Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
   Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.