The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Bonjour Tout le monde,
J'arrive pas a comprendre le "warning" résultant des definitions suivantes:

Module Type TITI.
Parameter X: Set.
End TITI.

Module Type Ex.
Declare Module t: TITI.
Parameter X : t.X -> t.X -> Set.
End Ex.

Module unionEx[X1: Ex; X2:Ex with Module t :=X1.t]: Ex.
Module t:X1.t.
Definition X :=[a,b:t.X] (X1.X a b)+(X2.X a b).
End unionEx.

Le warning qui s'affiche lors de la compilation est le suivant :
TODO:replace module after with!
Est ce qu'il y'a qq1 qui pourra m'aider comprendre le probleme?!
Je vous remercie d'avance
Cordialement

Houda ANOUN
LaBRI.