blob: 91e3df76ddca8e36d724feb14e96179433b4421a (
plain)
1
2
3
4
5
6
7
|
Set Universe Polymorphism.
Definition hProp : Type := sigT (fun _ : Type => True).
Goal Type.
Fail exact hProp@{Set}. (* test that it fails, but is not an anomaly *)
try (exact hProp@{Set}; fail 1). (* Toplevel input, characters 15-32:
Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
Please report. *)
|
