test-suite/bugs/closed/bug_13171.v


1
2
3
4
5
6
7
8
9
10

Primitive array := #array_type.

Goal False.
Proof.
  unshelve epose (_:nat). exact_no_check true.
  Fail let c := open_constr:([| n | 0 |]) in
       let c := eval cbv in c in
       let c := type of c in
       idtac c.
Abort.