The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

I'm having some trouble with the module system. This works fine:

  Require Import OrderedType OrderedTypeEx.

  Module A (OT : OrderedType).
    Definition x := 5.
  End A.

  Module A_nat := A Nat_as_OT.

But then when I save that file as A.v, and then create a new file B.v:

  Require Import OrderedType OrderedTypeEx.
  Require Import A.

  Module A_nat_2 := A Nat_as_OT.

Coq complains:

  User error: Application of not a functor

What am I doing wrong? Thanks!

Edsko