The Coq mailing list

[richard <richard.dapoigny AT univ-smb.fr>]

Dear Coq users,

I have first a module with a lot of lemmas and definitions:

Module  Mereo_signature (M1 : UsualDecidableTypeFull).
Import M1.

Definition ....

Lemma ...

Definition Universe : N := ...

End Mereo_signature.

Then, in a second module:

Module Topo_signature (M1 : UsualDecidableTypeFull).
Include Mereo_signature (M1).

...

Theorem int_space : (interior Universe) ≡ Universe.
Proof.

...

    Class Kuratowski_Open
      (X :Type)(Univ :X)(equiv_open : X -> X -> Prop)(Inter : X
      -> X -> X) := {
        Open                             : X -> Prop ;
        Interior                           : X -> X;
        open_space Univ          : equiv_open (Interior Univ) Univ;
      }.

Instance proof_topo : Kuratowski_Open N Universe singular_eq n_conjunction := {
  Open Q                                := exists a : N, η Q (klass a);
  Interior Q                              := interior Q;
  open_space Universe           := int_space;
}.

End Topo_signature.

I have the following error:

In Environment Universe: N The term "int_space" has type "interior Topo_signature.Universe = Topo_signature.Universe" while it is expected to have type "interior Universe = Universe".

If anyone has an idea to solve that difficulty?

Thanks in advance,

Richard