1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v
new file mode 100644
index 0000000000..0564722729
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13171.v
@@ -0,0 +1,10 @@
+Primitive array := #array_type.
+
+Goal False.
+Proof.
+  unshelve epose (_:nat). exact_no_check true.
+  Fail let c := open_constr:([| n | 0 |]) in
+       let c := eval cbv in c in
+       let c := type of c in
+       idtac c.
+Abort.