Fixing #4001 (missing type constraints when building return clause of match).

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4001.v b/test-suite/bugs/closed/4001.v
new file mode 100644
index 000000000..25d78f4b0
--- /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.