From 58e4f62915c50a2ad6f01acced636283ff5b4442 Mon Sep 17 00:00:00 2001
From: Yann Leray <yann.leray@inria.fr>
Date: Mon, 23 Oct 2023 10:35:59 +0200
Subject: [PATCH] Add test for bug #18194

---
 test-suite/bugs/bug_18194.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/bug_18194.v

diff --git a/test-suite/bugs/bug_18194.v b/test-suite/bugs/bug_18194.v
new file mode 100644
index 000000000000..12f10e9bbd97
--- /dev/null
+++ b/test-suite/bugs/bug_18194.v
@@ -0,0 +1,19 @@
+Require Import Coq.Program.Tactics.
+
+Program Definition a := Eval cbv zeta in (fun (a : True) => (?[A] : nat),
+  let r :=
+    let b := I in match tt with tt => b end
+  in
+  ?A@{a := r},
+  fun (a : True) => (eq_refl : ?A = _)).
+
+Next Obligation.
+  destruct a; exact 0.
+Defined.
+(* This used to fail with the message:
+File "test-suite/bugs/bug_18194.v", line 12, characters 0-8:
+Error:
+Unbound reference: In environment
+anonymous' : unit
+The reference 3 is free.
+*)