The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi everybody,
I still find a lot of problems while using Coq module system (V 7.4)
We consider for example what follows:

Module Type TIT.

Inductive X:Set:=
b:X.
End TIT.


Module Type TOTO.
Declare Module t:TIT.
Inductive titi:Set:=
a:t.X->titi.
End TOTO.


Module toto[ta:TOTO].
Module ti:=ta.t.

Definition ex1:(c,d:ti.X)(ta.a d)=(ta.a c) -> d=c.
Intros.
Injection H.

> > Injection H.
> > ^^^^^^^^^^^
>  
Error: Failed to decompose the equality


I wonder where is the problem here?!
Thanks for helping me to undestand this...
Houda.