The Coq mailing list

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

Dear coq members,

I have the following problem with importing definitions with multiples 
coq modules:

I have a file F1.v :
=====================================================================

Module  DST_signature (M1 : UsualDecidableTypeFull).
Import M1.
...
End DST_signature.
=====================================================================

then a file F2.v (there is a file F1.vo) :

=====================================================================
Require Import F1.

Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).

(** Module Abstract *Structure **)

Module geometry_signature (M1 : UsualDecidableTypeFull).

Module basis_mereo := Mereology M1.
Import basis_mereo.
...
End geometry_signature.
=====================================================================

and finally a file F3.v (there is a file F2.vo and a file F1.vo) :

=====================================================================

Require Import F1.
Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).

(** Module Abstract *Structure **)

Module AbstractStructure (M1 : UsualDecidableTypeFull).

Module basis_inst := Mereology M1.
Import basis_inst.
...
End  AbstractStructure.

Require Import F2.

Module Tarski_geom (M1 : UsualDecidableTypeFull).

Module basis_mereo := Mereology M1.
Import basis_mereo.
Module adt := AbstractStructure M1.
Import adt.
Module geom := geometry_signature M1.
Import geom.
...
Lemma test : forall A, η A balls -> η A (el Gspace). -> fail
...
End Tarski_geom.
=====================================================================

While there is no problem for all variables defined in F1 there seems to 
be a problem with variables  defined in F2 since the error is :

The term "Gspace" has type "basis_mereo.N" while it is expected to have 
type "N". (Gspace is defined in F2)

If someone has an idea to solve the problem?

Thanks in advance,

Richard