diff --git a/tests/gmap.ref b/tests/gmap.ref
index d0d2b38de6c8fe32dcac9ba473d354970065003b..71a0b12899e8250eaad1c6535902bfb55ed16287 100644
--- a/tests/gmap.ref
+++ b/tests/gmap.ref
@@ -70,10 +70,14 @@ Failed to progress.
   
   ============================
   bool_decide (∅ ⊆ {[1; 2; 3]}) = true
+"gmap_insert_comm"
+     : string
 1 goal
   
   ============================
   {[3 := false; 2 := true]} = {[2 := true; 3 := false]}
+"gmap_lookup_concrete"
+     : string
 1 goal
   
   ============================
diff --git a/tests/gmap.v b/tests/gmap.v
index 02b4c01b9ec8e6ced2f5fd8faab19a627c59905c..5973a432e00f5109251146c421db604c7315bfb5 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -1,4 +1,4 @@
-From stdpp Require Import pmap gmap.
+From stdpp Require Import strings pmap gmap.
 
 Goal {[1; 2; 3]} =@{gset nat} ∅.
 Proof.
@@ -120,10 +120,12 @@ Time Eval vm_compute in gmap_insert_positives_test 512000.
 Time Eval vm_compute in gmap_insert_positives_test 1000000.
 *)
 
+Check "gmap_insert_comm".
 Theorem gmap_insert_comm :
   {[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}.
 Proof. simpl. Show. reflexivity. Qed.
 
+Check "gmap_lookup_concrete".
 Theorem gmap_lookup_concrete :
   lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true.
 Proof. simpl. Show. reflexivity. Qed.