The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Richard, 

In F2.v you have a definition  *Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).*  and then the same in F3.v  *Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).*. I suspect when you redefining Mereology in F3 and subsequently importing F2.v, somehow it is causing some confusion.  Trying removing the definition *Module Mereology (M1 : UsualDecidableTypeFull) := DST_signature(M1).* from F3.v and see if it works (I am not an expert in modules so I cannot say for sure it is the case). 

Best, 

Mukesh 

On Sun, 22 Dec 2024 at 12:15, richard <richard.dapoigny AT univ-smb.fr> wrote:

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