aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3670.v
blob: c0f03261a9ffdad3108674dbdc1cc75b347ba79a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
Set Universe Polymorphism.
Module Type FOO.
  Parameter f : Type -> Type.
  Parameter h : forall T, f T.
End FOO.

Module Type BAR.
  Include FOO.
End BAR.

Module Type BAZ.
  Include FOO.
End BAZ.

Module BAR_FROM_BAZ (baz : BAZ) <: BAR.

  Definition f : Type -> Type. 
  Proof. exact baz.f. Defined.

  Definition h : forall T, f T.
  Admitted.

Fail End BAR_FROM_BAZ.