From 87779ac4be376a917dae2e4aabdd86980487db3e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 May 2022 11:54:43 +0200
Subject: [PATCH] Add test case.

---
 tests/gmap.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tests/gmap.v b/tests/gmap.v
index 3eb98b06..fff2df33 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -82,3 +82,10 @@ Proof.
   Fail progress simplify_eq.
   done.
 Qed.
+
+(** Test case for issue #139 *)
+
+Lemma test_issue_139 (m : gmap nat nat) : ∃ x, x ∉ dom m.
+Proof.
+  destruct (exist_fresh (dom m)); eauto.
+Qed.
-- 
GitLab