From cdaf8e2ed109bd117da2366a279fa575d7b6185a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Dec 2015 19:14:19 +0100
Subject: Fixing a pat%constr bug. Thanks to Enrico for reporting.

---
 test-suite/success/intros.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 17f160f98e..11156aa0ee 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -78,3 +78,9 @@ intros H2%H%H0.
 - exact H2.
 - exact H1.
 Qed.
+
+(* Bug found by Enrico *)
+
+Goal forall x : nat, True.
+intros y%(fun x => x).
+Abort.
-- 
cgit v1.2.3