Nous anticipons que la question de la transparence (pouvoir bénéficier de ce module de transfert tout en utilisant les tactiques habituelles de Coq) devrait nous conduire à repenser et généraliser le système des coercitions (conversions entre types) de Coq \cite{Sa_bi_1997}, ainsi que son intégration dans l'algorithme d'unification.