From fdfe3d31ee079046db8febe9e2a6ec0eebbf713d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2022 18:05:50 +0100
Subject: [PATCH] Test with custom inductive.

---
 tests/bi.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/bi.v b/tests/bi.v
index bab686754..c68be10a1 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -24,6 +24,12 @@ Definition big_sepM_pattern_value_tt
     {PROP : bi} (m : gmap nat ()) : PROP :=
   [∗ map] '() ∈ m, True.
 
+Inductive foo := Foo (n : nat).
+
+Definition big_sepM_pattern_value_custom
+    {PROP : bi} (m : gmap nat foo) : PROP :=
+  [∗ map] '(Foo x) ∈ m, ⌜ 10 = x ⌝.
+
 Definition big_sepM_pattern_key
     {PROP : bi} (m : gmap (nat * nat) nat) : PROP :=
   [∗ map] '(k,_) ↦ _ ∈ m, ⌜ 10 = k ⌝.
@@ -36,4 +42,4 @@ Definition big_sepM_cast {PROP : bi} (m : gmap nat nat) : PROP :=
   [∗ map] (x:nat) ∈ m, ⌜ 10%Z = x ⌝.
 
 Definition big_sepM2_pattern {PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP :=
-  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
\ No newline at end of file
+  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
-- 
GitLab