Test with custom inductive.

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 ⌝.