fixed the imports

src/MergeProduct.v

@@ -22,7 +22,7 @@ From mathcomp Require Import all_ssreflect.
 (** Merge operator *)
 Module MergeBig (s : SignatureParameter) (n : InfType).
 Module pp := ParallelProduct s n.
-Include pp.
+Import pp mup tp c leb eb b b.n b.s n s. 
 
 Definition bigraph_merge_product {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList} 
   (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2)

src/Nesting.v

@@ -23,7 +23,7 @@ Import ListNotations.
 (** Nesting operator *)
 Module NestingBig (s : SignatureParameter) (n : InfType).
 Module pp := ParallelProduct s n.
-Include pp.
+Import pp mup tp c leb eb b b.n b.s n s. 
 
 Definition nest {s1 r1 s2 r2 : nat} {o1 i2 o2 : NoDupList} 
   (b1 : bigraph s1 EmptyNDL r1 o1) (b2 : bigraph s2 i2 r2 o2) 

src/ParallelProduct.v

@@ -30,7 +30,7 @@ Require Import List.
   After the definition, we prove associativity and commutativity of dis_juxtaposition *)
 Module ParallelProduct (s : SignatureParameter) (n : InfType).
 Module mup := UnionPossible s n.
-Include mup.
+Import mup tp c leb eb b b.n b.s n s. 
 
 Set Typeclasses Unique Instances.
 Set Typeclasses Iterative Deepening.

src/Sorting.v

@@ -35,8 +35,8 @@ Import ListNotations.
 
 Module Sorting (s : SignatureParameter) (n : InfType).
 
-Module MB := MergeBig s n.
-Include MB. 
+Module mb := MergeBig s n.
+Import mb pp mup tp c leb eb b b.n b.s n s. 
 (* Parameter mysort:orderType tt. (*pourquoi tt et pas autre chose?*)
 Parameter DefautltSort:mysort. *)
 

src/UnionPossible.v

@@ -24,9 +24,8 @@ From mathcomp Require Import all_ssreflect.
 Require Import List.
 
 Module UnionPossible (s : SignatureParameter) (n : InfType).
-
 Module tp := TensorProduct s n.
-Include tp.
+Import tp c leb eb b b.n b.s n s. 
 
 Definition union_possible {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList} 
   (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) :=