fixed import on inftype and sigparam

src/AbstractBigraphs.v

@@ -36,9 +36,11 @@ Import ListNotations.
 
 (** This module implements bigraphs and basic operations on bigraphs *)
 Module Bigraphs (sp : SignatureParameter) (np : InfType).
+Import sp.
+Import np.
 Module s := Signature sp.
 Module n := infTs np.
-Include s.
+Import s.
 Import n.
 (** * Definition of a bigraph
   This section defines the Type bigraph *)
@@ -72,7 +74,7 @@ Definition get_control {s r : nat} {i o : NoDupList} (bg : bigraph s i r o) : ge
   @control s i r o bg.
 Definition get_parent {s r : nat} {i o : NoDupList} (bg : bigraph s i r o) : (get_node bg) + (ordinal s) -> (get_node bg) + (ordinal r) :=
   @parent s i r o bg.
-Definition get_link {s r : nat} {i o : NoDupList} (bg : bigraph s i r o) : {inner:np.infT | In inner i} + Port (@get_control s r i o bg) -> {outer:np.infT | In outer o} + (get_edge bg) :=
+Definition get_link {s r : nat} {i o : NoDupList} (bg : bigraph s i r o) : {inner:infT | In inner i} + Port (@get_control s r i o bg) -> {outer:infT | In outer o} + (get_edge bg) :=
   @link s i r o bg.
 Definition get_ap {s r : nat} {i o : NoDupList} (bg : bigraph s i r o) : FiniteParent (get_parent (bg:=bg)) := 
   @ap s i r o bg.
@@ -95,7 +97,7 @@ Theorem parent_proof_irrelevant {s i r o} (b:bigraph s i r o):
   Qed.
 
 Theorem innername_proof_irrelevant {s i r o} (b:bigraph s i r o): 
-  forall n:np.infT, forall Hn: In n i, forall Hn':In n i,
+  forall n:infT, forall Hn: In n i, forall Hn':In n i,
   get_link (bg:=b) (inl (exist _ n Hn)) = get_link (bg:=b) (inl (exist _ n Hn')).
   Proof. 
   intros. apply f_equal. apply f_equal. apply subset_eq_compat. reflexivity.
@@ -278,7 +280,7 @@ Definition symmetry_big (m:nat) (X:NoDupList) (n:nat) (Y:NoDupList) :
     destruct n'.
   Defined.
 
-Definition substitution (i:NoDupList) (name:np.infT) : bigraph 0 i 0 (OneelNDL name).
+Definition substitution (i:NoDupList) (name:infT) : bigraph 0 i 0 (OneelNDL name).
   Proof. 
   apply (@Big 0 i 0 (OneelNDL name)
     void (*node : ∅*)
@@ -293,10 +295,10 @@ Definition substitution (i:NoDupList) (name:np.infT) : bigraph 0 i 0 (OneelNDL n
   destruct n'.
   Defined.
 
-Definition elementary_renaming (n n':np.infT) := substitution (OneelNDL n) n'.
+Definition elementary_renaming (n n':infT) := substitution (OneelNDL n) n'.
 
 
-Definition closure (name:np.infT) : bigraph 0 (OneelNDL name) 0 EmptyNDL.
+Definition closure (name:infT) : bigraph 0 (OneelNDL name) 0 EmptyNDL.
   Proof. 
   apply (@Big 0 (OneelNDL name) 0 EmptyNDL
     void (*node : ∅*)

src/SignatureBig.v

@@ -8,18 +8,16 @@ Require Import FunctionalExtensionality.
 Require Import MathCompAddings.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finfun. 
+
 (** * This module implements a signature
   It contains a Module Type with Kappa and Arity, and Ports built from the Signature *)
 Module Type SignatureParameter.
-
   Parameter Kappa : eqType.
-(* Parameter EqDecK : forall x y : Kappa, {x = y} + {x <> y}. *)
   Parameter Arity : Kappa-> nat.
-
 End SignatureParameter.
 
-Module Signature (SP:SignatureParameter).
-Include SP.
+Module Signature (SParam:SignatureParameter).
+Import SParam.
 Definition Port {node : Type} (control : node -> Kappa): Type :=
   { n : node & 'I_(Arity (control n)) }.