From f70ecc5c943ef5d6b89104f0cf02ba38e5490607 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Mar 2020 15:30:23 +0100
Subject: [PATCH] Tests for `set_unfold in H`.

---
 tests/sets.ref | 0
 tests/sets.v   | 4 ++++
 2 files changed, 4 insertions(+)
 create mode 100644 tests/sets.ref
 create mode 100644 tests/sets.v

diff --git a/tests/sets.ref b/tests/sets.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/sets.v b/tests/sets.v
new file mode 100644
index 00000000..9aea1a62
--- /dev/null
+++ b/tests/sets.v
@@ -0,0 +1,4 @@
+From stdpp Require Import sets.
+
+Lemma foo `{Set_ A C} (x : A) (X Y : C) : x ∈ X ∩ Y → x ∈ X.
+Proof. intros Hx. set_unfold in Hx. tauto. Qed.
-- 
GitLab