aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_071.v
blob: b5a5ec1bda3ad1cffd3e8e92a877535586139876 (plain)
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.