From 3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 6 Sep 2014 12:13:03 +0200
Subject: Fix bug #3584, elaborating pattern-matching on primitive records to
 the use of projections.

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3584.v b/test-suite/bugs/closed/3584.v
new file mode 100644
index 0000000000..3d4660b487
--- /dev/null
+++ b/test-suite/bugs/closed/3584.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Definition eta_sigma {A} {P : A -> Type} (u : sigT P)
+  : existT _ (projT1 u) (projT2 u) = u
+  := match u with existT _ x y => eq_refl end. (* Toplevel input, characters 0-139:
+Error: Pattern-matching expression on an object of inductive type sigT
+has invalid information. *)
+Definition sum_of_sigT A B (x : sigT (fun b : bool => if b then A else B))
+: A + B
+  := match x with
+       | existT _ true a => inl a
+       | existT _ false b => inr b
+     end. (* Toplevel input, characters 0-182:
+Error: Pattern-matching expression on an object of inductive type sigT
+has invalid information. *)
\ No newline at end of file
-- 
cgit v1.2.3