aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3681.v
blob: 194113c6eda5214ae59746a304db924e385e0c2e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Module Type FOO.
  Parameters P Q : Type -> Type.
End FOO.

Module Type BAR.
  Declare Module Import foo : FOO.
  Parameter f : forall A, P A -> Q A -> A.
End BAR.

Module Type BAZ.
  Declare Module Export foo : FOO.
  Parameter g : forall A, P A -> Q A -> A.
End BAZ.

Module BAR_FROM_BAZ (baz : BAZ) : BAR.
  Import baz.
  Module foo <: FOO := foo.
  Import foo.
  Definition f : forall A, P A -> Q A -> A := g.
End BAR_FROM_BAZ.