The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Hello,

  You example works if you don't hide the field "a" in Constr.
  You can do that with the <: operator (Checks only module conformance
with Mm, but does no hiding).

Pierre


 Module Constr [U:Mm] <: Mm.


Carlos.SIMPSON wrote:
> Hi. Does anybody have any comments on the following behavior?  Is it a
> problem which will
> be fixed in a future release?
>
> ---Carlos Simpson
>
> Parameter A : Type.
>
> Parameter f : A -> A.
>
> Module Type Mm.
> Parameter a : A.
> End Mm.
>
> Module Constr [U:Mm] : Mm.
> Definition a := (f U.a).
>
> End Constr.
>
>
> Module Constr2 [V:Mm].
> Module Z := (Constr V).
> Module Z2 := Z.
> Module Z3 := (Constr V).
>
> Lemma lem1 : Z.a == Z2.a.
> Reflexivity.
> Save.
>
> Lemma lem2 : Z.a == Z3.a.
> Reflexivity.
>
> Toplevel input, characters 0-11
>
> > Reflexivity.
> > ^^^^^^^^^^^
>
> Error: Impossible to unify Z3.a with Z.a
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



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