Alain Frisch wrote:
>
> When applying a functor of type
> functor(X:S1) -> S2 to a module of type T, the module type for the
> result can be obtained in two different ways:
>
> (1) T is a path: the module type is obtained by substituting X with T in S2.
>
> (2) T is not a path: the module type is obtained by computing the
> smallest supertype of S2 that doesn't contain X anymore (under the extra
> assumption that X has type T).

I believe this doesn't type-check. :) You probably meant to say:

"When applying a functor of type
functor(X:S1) -> S2 to a module M of type T, the module type for the
result can be obtained in two different ways:

(1) M is a path: the module type is obtained by substituting X with M in S2.

(2) M is not a path: the module type is obtained by computing the
smallest supertype of S2 that doesn't contain X anymore (under the extra
assumption that X has type T)."

/Andreas