test-suite/modules/SeveralWith.v


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

Module Type S.
Parameter A : Type.
End S.

Module Type ES.
Parameter A : Type.
Parameter eq : A -> A -> Type.
End ES.

Module Make
  (AX : S)
  (X : ES with Definition A := AX.A with Definition eq := @eq AX.A).
End Make.