path: root/test-suite/bugs/opened/HoTT_coq_114.v

Fail Inductive test : $(let U := type of Type in exact U)$ := t.
(* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *)