test-suite/bugs/closed/HoTT_coq_071.v


1
2
3
4
5
6
7
8
9

Set Universe Polymorphism.
Definition foo : True.
  abstract exact I.
Defined.
Eval hnf in foo. (* Should not be [I] *)
Goal True.
Proof.
  Fail unify foo I.
Abort.