From 1b43dfcb6facbc88c611db3ecb9076e377eebb34 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Nov 2020 00:10:07 +0100
Subject: Removing flag "Bracketing Last Introduction Pattern".

---
 test-suite/bugs/closed/bug_4787.v | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 test-suite/bugs/closed/bug_4787.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_4787.v b/test-suite/bugs/closed/bug_4787.v
deleted file mode 100644
index a1444a4f63..0000000000
--- a/test-suite/bugs/closed/bug_4787.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* [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