The Coq mailing list

[Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>]

On Mon, Jan 12, 2004 at 01:03:15PM +0100, Houda Anoun wrote:
> Hi everybody,
> I find a lot of problems while using notations defined inside functors , 
> in fact sometimes these notations are not activated and I can't 
> undestand why?
> Here is a simpl example that illutrates what I said:
> 
> ------------------------------------------------------------------------
> 
> Module Type SIGNot.
> Inductive InfTwoNat:nat-> Prop:=
> ohConstructorTooLong: forall (n:nat), n<2%nat ->InfTwoNat n.
> End SIGNot.
> 
> Module sigImpl <:SIGNot.
> Inductive InfTwoNat:nat ->Prop:=
> ohConstructorTooLong: forall (n:nat), n<2%nat ->InfTwoNat n.
> 
> Notation "<<< n A" :=(ohConstructorTooLong n A ) (at level 40).
> End sigImpl.
> 
> Module Ext (picsou:SIGNot).
> Module T:=picsou.
> End Ext.
> 
> Module ExtImpl:=Ext sigImpl.
> 
> Import ExtImpl.
> Import sigImpl.
> 
> Lemma tooeasy:0%nat < 2%nat.
> 
> auto.
> Qed.
> 
> Check ohConstructorTooLong 0%nat tooeasy.
> (*
> <<< 0 tooeasy
>      : InfTwoNat 0
> 
> In this case there is no problem at all
> 
> *)
> 
> Check ExtImpl.T.ohConstructorTooLong 0%nat tooeasy.
> (* 
> 
> T.ohConstructorTooLong 0 tooeasy
>      : T.InfTwoNat 0
> 
> Whereas here, the notation is not activated but why??!
> *)
> 
> As we all see, we have ExtImpl.T=sigImpl, but it seems to me that the
> system can't unify between these modules even if there are equal.

The module type assigned to ExtImpl.T is SIGnot
(Module T:=picsous is a shortcut for Module T:SIGnot/picsou:=picsou)
so notations for ExtImpl.T come frm SIGnot
and not sigImp.

The above is also valid for Auto hints, declarations of coercions, setoids
and all other extralogical components of Coq.


> Is this a bug ?

No, that is a feature :)

Seriously, in situations like this one:
Module M:T:=A
one has to decide which elements come from T and which from A.
Now they simply all come from T.

> Thanks for helping me 

Hope this helps

Jacek