From 61284d21573b4d447d5bfada6a914f0bdfed7505 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Dec 2022 13:02:03 +0100
Subject: [PATCH] Add test.

---
 tests/decidable.ref |  2 ++
 tests/decidable.v   | 11 +++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 tests/decidable.ref
 create mode 100644 tests/decidable.v

diff --git a/tests/decidable.ref b/tests/decidable.ref
new file mode 100644
index 00000000..5f8d2cc7
--- /dev/null
+++ b/tests/decidable.ref
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+No applicable tactic.
diff --git a/tests/decidable.v b/tests/decidable.v
new file mode 100644
index 00000000..e192d182
--- /dev/null
+++ b/tests/decidable.v
@@ -0,0 +1,11 @@
+From stdpp Require Import list.
+
+(** Test that Coq does not infer [x ∈ xs] as [False] by eagerly using
+[False_dec] on a goal with unresolved type class instances. *)
+Example issue_165 (x : nat) :
+  ¬ ∃ xs : list nat, (guard (x ∈ xs); Some x) ≠ None.
+Proof.
+  intros [xs Hxs]. case_option_guard; [|done].
+  Fail done. (* Would succeed if the instance backing [x ∈ xs] is infered as
+  [False]. *)
+Abort.
-- 
GitLab