From e28be21112c174a4c1a84d45a50745f0ad4e646a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 18 Feb 2016 19:55:35 +0100
Subject: Fixing a bug with introduction patterns over inductive types
 containing let-ins.

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

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 69d66f1008..af5f994010 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -98,3 +98,10 @@ intros x ->.
 - reflexivity.
 - exact I.
 Qed.
+
+(* Fixing a bug when destructing a type with let-ins in the constructor *)
+
+Inductive I := C : let x:=1 in x=1 -> I.
+Goal I -> True.
+intros [x H]. (* Was failing in 8.5 *)
+Abort.
-- 
cgit v1.2.3