The Coq mailing list

["Patricia Peratto" <psperatto AT adinet.com.uy>]

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

To: Patricia Peratto

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> 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