The Coq mailing list

[Thomas Dinsdale-Young <td202 AT doc.ic.ac.uk>]

In

Module Program1 (Import X:HasEq).

the reason X is not a module is that HasEq is the type of a functor, 
rather than the type of a module.  If T is a module of type Typ, then 
HasEq T is a module type.  (T is a module that just consists of a type 
called t.  HasEq T is the type of modules that consist of a relation eq 
on the type t.  HasEq is the type of functors that given a module of 
type T produce a module with a relation eq on the type T.t.)

You may want to write something like

Module Program1 (Import T : Typ) (Import X : HasEq T).

The Import imports the namespace of the module into the current module, 
so you can directly reference t and eq.  Otherwise, you would have to 
write T.t and X.eq.

Hope this helps
-- Thomas

On 12/06/2012 16:01, Patricia Peratto wrote:
> Can someone explain me why in some cases one has to write
> the word Import by example in
> Module Type HasEq (Import T:Typ).
> in module Equalities
> and not in other cases?
> Regards Patricia
> ----- Original Message -----
> *From:* Sylvain Heraud 
> <mailto:sylvain.heraud AT gmail.com>
> *To:* Patricia Peratto 
> <mailto:psperatto AT adinet.com.uy>
> *Sent:* Monday, June 11, 2012 12:05 PM
> *Subject:* Re: [Coq-Club] module
>
> You have to remove the keyword Import !
> Module Program1 (X:HasEq).
>
> Sylvain
>
> On Sun, Jun 10, 2012 at 8:03 PM, Patricia Peratto
> <psperatto AT adinet.com.uy
>  
> <mailto:psperatto AT adinet.com.uy>>
>  wrote:
>
>     __
>     Forgive me by the questions I make but I'm in my
>     first Coq proof.
>     I have imported Coq.Structures.Equalities. and
>     below it I import a Module with
>     Module Program1 (Import X:HasEq).
>     and Coq displays the message:
>     Error:X is not a module
>     but HasEq was defined in Equalities.
>     Regards
>     Patricia