test-suite/bugs/closed/bug_7967.v


1
2
3
4
5
6

Set Universe Polymorphism.
Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A.

(* A similar bug *)
Context (C := ltac:(let y := constr:(Type) in exact nat)).
Check C@{}.