From a0970a6bef365a31ae780f2b7d673f5f4ae37aa9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Jun 2016 16:08:05 +0200
Subject: Test for #4787.

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

diff --git a/test-suite/bugs/closed/4787.v b/test-suite/bugs/closed/4787.v
new file mode 100644
index 0000000000..b586cba50f
--- /dev/null
+++ b/test-suite/bugs/closed/4787.v
@@ -0,0 +1,9 @@
+(* [Unset Bracketing Last Introduction Pattern] was not working *)
+
+Unset Bracketing Last Introduction Pattern.
+
+Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y.
+do 10 ((intros [] || intro); simpl); reflexivity.
+Qed.
+
+
-- 
cgit v1.2.3