aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/5996.v
blob: c9e3292b481c0de5a651022b04b6fff792704018 (plain)
1
2
3
4
5
6
7
8
Goal Type.
  let c := constr:(prod nat nat) in
  let c' := (eval pattern nat in c) in
  let c' := lazymatch c' with ?f _ => f end in
  let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in
  let _ := type of c'' in
  exact c''.
Defined.