summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2342.v
blob: 094e5466cb5537687d8321943106dd329c16ff51 (plain)
1
2
3
4
5
6
7
8
(* Checking that the type inference algoithme does not commit to an
   equality over sorts when only a subtyping constraint is around *)

Parameter A : Set.
Parameter B : A -> Set.
Parameter F : Set -> Prop. 
Check (F (forall x, B x)).