test-suite/bugs/closed/bug_13732.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Module Sort.
  Set Printing Universes.

  Implicit Types TT : Type.

  Check fun TT => nat.
End Sort.

Module Ref.
  Set Universe Polymorphism.

  Axiom tele : Type.

  Implicit Types TT : tele.
  Check fun TT => nat.
End Ref.