test-suite/bugs/closed/bug_11048.v


1
2
3
4
5

Inductive foo (HUGE := _) (b : HUGE) A :=
  bar (X:match _ : HUGE as T return HUGE with T => match (A : T) -> True with _ => T end end)
  : foo b A.
(* uncaught destKO *)