From 8d18a7712fad4d869db1257dbcd08460c14b11e9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 23:59:44 +0200
Subject: [PATCH] Tweak tests.

---
 tests/gmap.ref | 4 ++++
 tests/gmap.v   | 4 +++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/gmap.ref b/tests/gmap.ref
index d0d2b38d..71a0b128 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 02b4c01b..5973a432 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.
-- 
GitLab