From a110ddfd6fc040a805de3f0ec2995b51ff301f5c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Dec 2015 11:31:13 +0100
Subject: Adding a test for the unshelve tactical.

---
 test-suite/success/unshelve.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/success/unshelve.v

diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v
new file mode 100644
index 0000000000..672222bdd6
--- /dev/null
+++ b/test-suite/success/unshelve.v
@@ -0,0 +1,11 @@
+Axiom F : forall (b : bool), b = true ->
+  forall (i : unit), i = i -> True.
+
+Goal True.
+Proof.
+unshelve (refine (F _ _ _ _)).
++ exact true.
++ exact tt.
++ exact (@eq_refl bool true).
++ exact (@eq_refl unit tt).
+Qed.
-- 
cgit v1.2.3