1 files changed, 36 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3217.v b/test-suite/bugs/closed/3217.v
new file mode 100644
index 00000000..ec846bf9
--- /dev/null
+++ b/test-suite/bugs/closed/3217.v
@@ -0,0 +1,36 @@
+(** [Set Implicit Arguments] causes Coq to run out of memory on [Qed] before c3feef4ed5dec126f1144dec91eee9c0f0522a94 *)
+Set Implicit Arguments.
+
+Variable LEM: forall P : Prop, sumbool P (P -> False).
+
+Definition pmap := option (nat -> option nat).
+
+Definition pmplus (oha ohb: pmap) : pmap :=
+ match oha, ohb with
+ | Some ha, Some hb =>
+   if LEM (oha = ohb) then None else None
+ | _, _ => None
+ end.
+
+Definition pmemp: pmap := Some (fun _ => None).
+
+Lemma foo:
+ True ->
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+    (pmplus pmemp
+     pmemp))))))))))))
+    =
+    None -> True.
+Proof.
+  auto.
+Timeout 2 Qed.