From 272d3554e6e6e4f4a467ef820a9f14cdfa3b3ad1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Mar 2018 14:23:12 +0100
Subject: [PATCH] add a test for TC resolution not happening too early

---
 theories/tests/proofmode.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 042948250..5d5e8dff1 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -166,6 +166,15 @@ Proof.
   iSpecialize ("H" $! _ [#10]). done.
 Qed.
 
+(* Check that typeclasses are not resolved too early *)
+Lemma test_TC_resolution `{!BiAffine PROP} (Φ : nat → PROP) l x :
+  x ∈ l → ([∗ list] y ∈ l, Φ y) -∗ Φ x.
+Proof.
+  iIntros (Hp) "HT".
+  iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
+  done.
+Qed.
+
 Lemma test_eauto_iFrame P Q R `{!Persistent R} :
   P -∗ Q -∗ R → R ∗ Q ∗ P ∗ R ∨ False.
 Proof. eauto 10 with iFrame. Qed.
-- 
GitLab