The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

It seems that applying the same functor to the same modules
don't give you the same module.


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 Nat.
 Definition  X := nat.
End Nat.

Module A := toto Nat.
Module B := toto Nat.
Check A.t1.
Check B.t1.

Check (a:Nat.X)(A.t1 a)=(B.t1 a).
Error: In environment
a : Nat.X
The term (B.t1 a) has type (B.titi a) while it is expected to have type
 (A.titi a)


Perhaps it is an answer to your problem.

Note that in Ocaml the same constructions allow to compare elements
of types B.titi and A.titi.


--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran