From 525c0e434e9b9472b6249bfd575659eb2dbec206 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Feb 2015 21:54:21 +0100
Subject: Fixing #4001 (missing type constraints when building return clause of
 match).

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4001.v b/test-suite/bugs/closed/4001.v
new file mode 100644
index 0000000000..25d78f4b0e
--- /dev/null
+++ b/test-suite/bugs/closed/4001.v
@@ -0,0 +1,18 @@
+(* Computing the type constraints to be satisfied when building the
+   return clause of a match with a match *)
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+  
+Variable A : Type.
+Variable typ : A -> Type.
+
+Inductive t : list A -> Type :=
+| snil  : t nil
+| scons : forall (x : A) (e : typ x) (lx : list A) (le : t  lx), t (x::lx).
+
+Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
+  match s in t l'  with
+  | snil => False
+  | scons _ e _ _ => e
+  end.
-- 
cgit v1.2.3