The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Bonjour,
J'ai tjrs beaucoup de problemes quand j'utilise le systeme des modules 
et je me demande si ce sont des bugs ou pas...
Entre autres , on considere l'exemple suivant:

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

Module toto[t:TOTO].
Inductive titi :t.X ->Set:=
t1: (a:t.X) (titi a).
End toto.

Module kiki[t:TOTO].
Module to:=toto t.
Definition t':(a:t.X) (to.titi a).
Constructor 1.
Defined.
End kiki.

Module koukou[t:TOTO].
Module ki:=kiki t.
Module to':=toto t.

Definition def:(a:t.X) (to'.titi a).
Intro; Apply ki.t'.


Logiquement, ceci doit marcher étant donné que le module to' est 
confondu avec ki.to non?!
Malheureusement, c'est pas le cas , en effet j'obtiens l'erreur suivante:

Toplevel input, characters 0-11
> Apply ki.t'.
> ^^^^^^^^^^^

Error: Impossible to unify (ki.to.titi ?3) with (to'.titi a)

Y'a t'il qq1 qui peut m'expliquer pkoi?
Je vous remercie d'avance...
Cordialement
Houda ANOUN
LaBRI.