The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Hi,

My problem is in Module Type T3 below.

Module Type T1.
Parameter A : Set.
Parameter a : A.
End T1.

Module Type T2 (M1:T1).
Parameter f : M1.A -> M1.A.
End T2.

Module Type T3 (M1:T1) (M2:T2).
Parameter prop : M2(M1).f M1.a = M1.a.
(* doesn' work ! *)
(* I've tried to add 
Declare Module M' := M2(M1)
But i receive "Only simple modules allowed in module declarations"... *)

End T3.


I there a way to do similar things with the Coq module system ?

Thanks,

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
David Pichardie
http://www.irisa.fr/lande/pichardie/index.en.html