> This means that if I want to export T1 and T2 then I have to write as
>  module M1 : sig type t = M.t = T1 | T2 end = M
> Is it correct?

Yes it is. It is exactly what J.C. Filliâtre propose.

> In my situation, M defines many types and many type constructors,
> and I want to give M different signatures, each of which will export
> different sets of type constructors.
> Then, it seems that I have to write the same type constructor declarations
> a number of times....
> Isn't it avoidable?

You can use the "include" statement:

module M = struct type s = S type t = T1 | T2 end
module type S = sig type s = M.s = S end
module type T = sig type t = M.t = T1 | T2 end
module type ST = sig include S include T end
module MS : S = M
module MT : T = M
module MST : ST = M

Julien
-- 
mailto:Julien.Signoles@lri.fr ; http://www.lri.fr/~signoles
"In theory, practice and theory are the same,
but in practice they are different" (Larry McVoy)