Imported Upstream version 8.5~beta1+dfsg

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3584.v b/test-suite/bugs/closed/3584.v
new file mode 100644
index 00000000..3d4660b4
--- /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