From 968c8af13deaa3871aca7fc7086f1a5dc5769fde Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Apr 2015 17:34:09 +0200
Subject: Add test-suite file for bug #4120.

---
 test-suite/bugs/closed/4120.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/4120.v

diff --git a/test-suite/bugs/closed/4120.v b/test-suite/bugs/closed/4120.v
new file mode 100644
index 0000000000..4164d86dc1
--- /dev/null
+++ b/test-suite/bugs/closed/4120.v
@@ -0,0 +1,6 @@
+Definition id {T} (x : T) := x.
+Goal sigT (fun x => id x)%type.
+  change (fun x => ?f x) with f.
+  Unshelve.
+  exists Type. exact Set.
+Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
\ No newline at end of file
-- 
cgit v1.2.3