From 5bb473516020ce2bd9a510160fac22e2262c6915 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Feb 2022 15:45:37 +0100
Subject: [PATCH] Tests.

---
 tests/gmap.ref |  6 ++++++
 tests/gmap.v   | 14 ++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/tests/gmap.ref b/tests/gmap.ref
index a4d42549..8b1fa98f 100644
--- a/tests/gmap.ref
+++ b/tests/gmap.ref
@@ -70,3 +70,9 @@ Failed to progress.
   
   ============================
   bool_decide (∅ ⊆ {[1; 2; 3]}) = true
+The command has indeed failed with message:
+Nothing to inject.
+The command has indeed failed with message:
+Nothing to inject.
+The command has indeed failed with message:
+Failed to progress.
diff --git a/tests/gmap.v b/tests/gmap.v
index 6cb7029b..987c0fe6 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -68,3 +68,17 @@ Proof.
   Show.
   reflexivity.
 Qed.
+
+Lemma should_not_unfold (m1 m2 : gmap nat nat) k x :
+  dom (gset nat) m1 = dom (gset nat) m2 →
+  <[k:=x]> m1 = <[k:=x]> m2 →
+  True.
+Proof.
+  (** Make sure that [injection]/[simplify_eq] does not unfold constructs on
+  [gmap] and [gset]. *)
+  intros Hdom Hinsert.
+  Fail injection Hdom.
+  Fail injection Hinsert.
+  Fail progress simplify_eq.
+  done.
+Qed.
-- 
GitLab