test-suite/bugs/closed/5641.v


1
2
3
4
5
6

Set Universe Polymorphism.

Definition foo@{i j} (A : Type@{i}) : Type@{j}.
Proof.
abstract (exact ltac:(abstract (exact A))).
Defined.