From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 Sep 2009 10:23:45 +0000 (+0000)
Subject: some renaming. final commit for version 0.8.0
X-Git-Tag: make_still_working~3465
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3cddcf163b36101158ea33b3fad368ac8c62d75;p=helm.git

some renaming. final commit for version 0.8.0
---

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 9e2f23a6f..8ee2db5d8 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -21,14 +21,14 @@ common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi
 common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi 
 common/output.cmo: lib/log.cmi common/output.cmi 
 common/output.cmx: lib/log.cmx common/output.cmi 
-common/unit.cmo: lib/nUri.cmi automath/aut.cmx 
-common/unit.cmx: lib/nUri.cmx automath/aut.cmx 
-common/library.cmi: common/unit.cmx common/hierarchy.cmi 
+common/entity.cmo: lib/nUri.cmi automath/aut.cmx 
+common/entity.cmx: lib/nUri.cmx automath/aut.cmx 
+common/library.cmi: common/hierarchy.cmi common/entity.cmx 
 common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi 
 common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi 
-basic_rg/brg.cmo: common/unit.cmx 
-basic_rg/brg.cmx: common/unit.cmx 
-basic_rg/brgOutput.cmi: common/unit.cmx lib/log.cmi basic_rg/brg.cmx 
+basic_rg/brg.cmo: common/entity.cmx 
+basic_rg/brg.cmx: common/entity.cmx 
+basic_rg/brgOutput.cmi: lib/log.cmi common/entity.cmx basic_rg/brg.cmx 
 basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
     common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
 basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
@@ -66,8 +66,8 @@ basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \
 basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \
     basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
     basic_rg/brgUntrusted.cmi 
-basic_ag/bag.cmo: common/unit.cmx lib/log.cmi lib/cps.cmx 
-basic_ag/bag.cmx: common/unit.cmx lib/log.cmx lib/cps.cmx 
+basic_ag/bag.cmo: lib/log.cmi common/entity.cmx lib/cps.cmx 
+basic_ag/bag.cmx: lib/log.cmx common/entity.cmx lib/cps.cmx 
 basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx 
 basic_ag/bagOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
     common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi 
@@ -104,8 +104,8 @@ basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \
     basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi 
 basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \
     basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi 
-toplevel/meta.cmo: common/unit.cmx 
-toplevel/meta.cmx: common/unit.cmx 
+toplevel/meta.cmo: common/entity.cmx 
+toplevel/meta.cmx: common/entity.cmx 
 toplevel/metaOutput.cmi: toplevel/meta.cmx 
 toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \
     lib/cps.cmx toplevel/metaOutput.cmi 
diff --git a/helm/software/lambda-delta/automath/Omega.aut b/helm/software/lambda-delta/automath/Omega.aut
index 661154db9..2466a606e 100644
--- a/helm/software/lambda-delta/automath/Omega.aut
+++ b/helm/software/lambda-delta/automath/Omega.aut
@@ -2,7 +2,7 @@
 # This book is not accepted in AUT-QE because [y:'type'] is not allowed
 # This book is accepted in lambda-delta with sort inclusion but Omega is not
 #    valid if sort inclusion is allowed on the term backbone only
-# This book is valid in lambda-delta with sort inclusion allowed everywhere 
+# This book is valid in lambda-delta with unrestricted sort inclusion 
 
 +l 
 @ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
diff --git a/helm/software/lambda-delta/automath/aut.ml b/helm/software/lambda-delta/automath/aut.ml
index d05e53d03..513bd4a47 100644
--- a/helm/software/lambda-delta/automath/aut.ml
+++ b/helm/software/lambda-delta/automath/aut.ml
@@ -16,10 +16,10 @@ type qid = id * bool * id list (* qualified identifier: name, local?, path *)
 type term = Sort of bool              (* sorts: true = TYPE, false = PROP *)
 	  | GRef of qid * term list   (* reference: name, arguments *)
 	  | Appl of term * term       (* application: argument, function *)
-	  | Abst of id * term * term  (* abstraction: name, type, body *)
+	  | Abst of id * term * term  (* abstraction: name, domain, scope *)
 	  
-type unit = Section of (bool * id) option  (* section: Some true = open, Some false = reopen, None = close last *)
-	  | Context of qid option          (* context: Some = last node, None = root *)
-	  | Block of id * term             (* block opener: name, type *)
-	  | Decl of id * term              (* declaration: name, type *)
-	  | Def of id * term * bool * term (* definition: name, type, transparent?, body *)
+type entity = Section of (bool * id) option  (* section: Some true = open, Some false = reopen, None = close last *)
+	    | Context of qid option          (* context: Some = last node, None = root *)
+	    | Block of id * term             (* block opener: name, domain *)
+	    | Decl of id * term              (* declaration: name, domain *)
+	    | Def of id * term * bool * term (* definition: name, domain, transparent?, body *)
diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml
index f9467d63e..5b415ff0b 100644
--- a/helm/software/lambda-delta/automath/autOutput.ml
+++ b/helm/software/lambda-delta/automath/autOutput.ml
@@ -50,7 +50,7 @@ let rec count_term f c = function
       let f c = count_term f c t in
       count_term f c w
 
-let count_unit f c = function
+let count_entity f c = function
    | A.Section _        ->
       f {c with sections = succ c.sections}
    | A.Context _        ->
@@ -68,14 +68,14 @@ let count_unit f c = function
 
 let print_counters f c =
    let terms = c.sorts + c.grefs + c.appls + c.absts in
-   let units = c.sections + c.contexts + c.blocks + c.decls + c.defs in
+   let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in
    L.warn (P.sprintf "  Automath representation summary");
-   L.warn (P.sprintf "    Total book units:         %7u" units);
-   L.warn (P.sprintf "      Section units:          %7u" c.sections);
-   L.warn (P.sprintf "      Context units:          %7u" c.contexts);
-   L.warn (P.sprintf "      Block units:            %7u" c.blocks);
-   L.warn (P.sprintf "      Declaration units:      %7u" c.decls);
-   L.warn (P.sprintf "      Definition units:       %7u" c.defs);
+   L.warn (P.sprintf "    Total book entities:      %7u" entities);
+   L.warn (P.sprintf "      Section entities:       %7u" c.sections);
+   L.warn (P.sprintf "      Context entities:       %7u" c.contexts);
+   L.warn (P.sprintf "      Block entities:         %7u" c.blocks);
+   L.warn (P.sprintf "      Declaration entities:   %7u" c.decls);
+   L.warn (P.sprintf "      Definition entities:    %7u" c.defs);
    L.warn (P.sprintf "    Total Parameter items:    %7u" c.pars);
    L.warn (P.sprintf "      Application items:      %7u" c.pars);
    L.warn (P.sprintf "    Total term items:         %7u" terms);
diff --git a/helm/software/lambda-delta/automath/autOutput.mli b/helm/software/lambda-delta/automath/autOutput.mli
index fb02ed2d8..611c1bf6b 100644
--- a/helm/software/lambda-delta/automath/autOutput.mli
+++ b/helm/software/lambda-delta/automath/autOutput.mli
@@ -13,7 +13,7 @@ type counters
 
 val initial_counters: counters
 
-val count_unit: (counters -> 'a) -> counters -> Aut.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Aut.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly
index f974b9808..c772837b3 100644
--- a/helm/software/lambda-delta/automath/autParser.mly
+++ b/helm/software/lambda-delta/automath/autParser.mly
@@ -32,7 +32,7 @@
    %token TYPE PROP DEF EB E PN EXIT
     
    %start book
-   %type <Aut.unit list> book   
+   %type <Aut.entity list> book   
 %%
    path: MINUS {} | FS {} ;
    oftype: CN {} | CM {} ;
@@ -71,7 +71,7 @@
       | term          { [$1]     }
       | term CM terms { $1 :: $3 }
    ;
-   unit:
+   entity:
       | PLUS IDENT                    { A.Section (Some (true, $2))  }
       | PLUS TIMES IDENT              { A.Section (Some (false, $3)) }
       | MINUS IDENT                   { A.Section None               }
@@ -86,10 +86,10 @@
       | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4)       }
       | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6)       }
    ;
-   units:
-      |            { []       }
-      | unit units { $1 :: $2 }
+   entities:
+      |                 { []       }
+      | entity entities { $1 :: $2 }
    ;
    book:
-      | units eof { $1 }
+      | entities eof { $1 }
    ;
diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml
index 56ecd4ca4..0009e021e 100644
--- a/helm/software/lambda-delta/automath/autProcess.ml
+++ b/helm/software/lambda-delta/automath/autProcess.ml
@@ -57,12 +57,12 @@ let proc_global f st =
    in
    exp_count f st
 
-let proc_unit f st unit = match unit with
-   | A.Section section -> proc_section f st section unit
-   | A.Context _       -> proc_context f st unit  
-   | A.Block _         -> proc_block f st unit
-   | A.Decl _          -> proc_global f st unit
-   | A.Def _           -> proc_global f st unit
+let proc_entity f st entity = match entity with
+   | A.Section section -> proc_section f st section entity
+   | A.Context _       -> proc_context f st entity  
+   | A.Block _         -> proc_block f st entity
+   | A.Decl _          -> proc_global f st entity
+   | A.Def _           -> proc_global f st entity
    
 (* interface functions ******************************************************)
 
@@ -72,6 +72,6 @@ let initial_status = {
    iao = 0; iar = 0; iac = 0; iag = 0
 }
 
-let process_unit = proc_unit
+let process_entity = proc_entity
 
 let get_counters f st = f st.iao st.iar st.iac st.iag
diff --git a/helm/software/lambda-delta/automath/autProcess.mli b/helm/software/lambda-delta/automath/autProcess.mli
index e84f91aee..8f10b653e 100644
--- a/helm/software/lambda-delta/automath/autProcess.mli
+++ b/helm/software/lambda-delta/automath/autProcess.mli
@@ -13,6 +13,6 @@ type status
 
 val initial_status: status
 
-val process_unit: (status -> Aut.unit -> 'a) -> status -> Aut.unit -> 'a
+val process_entity: (status -> Aut.entity -> 'a) -> status -> Aut.entity -> 'a
 
 val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a
diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml
index 3fa4568d1..79e7a0421 100644
--- a/helm/software/lambda-delta/basic_ag/bag.ml
+++ b/helm/software/lambda-delta/basic_ag/bag.ml
@@ -12,8 +12,8 @@
 (* kernel version: basic, absolute, global *)
 (* note          : experimental *) 
 
-type uri = Unit.uri
-type id = Unit.id
+type uri = Entity.uri
+type id = Entity.id
 
 type bind = Void         (* exclusion *)
           | Abst of term (* abstraction *)
@@ -22,13 +22,13 @@ type bind = Void         (* exclusion *)
 and term = Sort of int                    (* hierarchy index *)
          | LRef of int                    (* location *)
          | GRef of uri                    (* reference *)
-         | Cast of term * term            (* type, term *)
+         | Cast of term * term            (* domain, element *)
          | Appl of term * term            (* argument, function *)
          | Bind of int * id * bind * term (* location, name, binder, scope *)
 
-type entry = bind Unit.entry (* age, uri, binder *)
+type entry = bind Entity.entry (* age, uri, binder *)
 
-type unit = bind Unit.unit
+type entity = bind Entity.entity
 
 type lenv = (int * id * bind) list (* location, name, binder *) 
 
diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml
index eb3bf05d9..400ffc55e 100644
--- a/helm/software/lambda-delta/basic_ag/bagOutput.ml
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml
@@ -74,7 +74,7 @@ let count_entry_binder f c = function
 let count_entry f c (_, _, b) =
    count_entry_binder f c b
 
-let count_unit f c = function
+let count_entity f c = function
    | Some entry -> count_entry f c entry
    | None     -> f c
 
diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli
index f3761ac1a..daa07a6d1 100644
--- a/helm/software/lambda-delta/basic_ag/bagOutput.mli
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.mli
@@ -13,7 +13,7 @@ type counters
 
 val initial_counters: counters
 
-val count_unit: (counters -> 'a) -> counters -> Bag.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli
index 76ba89918..9aa4ec575 100644
--- a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli
+++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli
@@ -10,5 +10,5 @@
       V_______________________________________________________________ *)
 
 val type_check:
-   (Bag.term option -> Bag.unit -> 'a) -> ?si:bool ->
-   Hierarchy.graph -> Bag.unit -> 'a
+   (Bag.term option -> Bag.entity -> 'a) -> ?si:bool ->
+   Hierarchy.graph -> Bag.entity -> 'a
diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index d0a442807..e3c586681 100644
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -12,8 +12,8 @@
 (* kernel version: basic, relative, global *)
 (* note          : ufficial basic lambda-delta *) 
 
-type uri = Unit.uri
-type id = Unit.id
+type uri = Entity.uri
+type id = Entity.id
 
 type attr = Name of bool * id  (* real?, name *)
           | Apix of int        (* additional position index *)
@@ -31,9 +31,9 @@ and term = Sort of attrs * int         (* attrs, hierarchy index *)
          | Appl of attrs * term * term (* attrs, argument, function *)
          | Bind of bind * term         (* binder, scope *)
 
-type entry = bind Unit.entry (* age, uri, binder *)
+type entry = bind Entity.entry (* age, uri, binder *)
 
-type unit = bind Unit.unit
+type entity = bind Entity.entity
 
 type lenv = Null
 (* Cons: tail, relative local environment, binder *) 
diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index 1a0b0650e..662a71988 100644
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -103,7 +103,7 @@ let count_entry f c = function
       } in
       f c
 
-let count_unit f c = function
+let count_entity f c = function
    | Some entry -> count_entry f c entry
    | None     -> f c
 
diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli
index b9acfd302..0af895dd4 100644
--- a/helm/software/lambda-delta/basic_rg/brgOutput.mli
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli
@@ -13,10 +13,10 @@ type counters
 
 val initial_counters: counters
 
-val count_unit: (counters -> 'a) -> counters -> Brg.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Brg.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
 val specs: (Brg.lenv, Brg.term) Log.specs
 
-val export_entry: Format.formatter -> Brg.bind Unit.entry -> unit
+val export_entry: Format.formatter -> Brg.bind Entity.entry -> unit
diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli
index 80f9b2eee..bab64303e 100644
--- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli
+++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli
@@ -10,5 +10,5 @@
       V_______________________________________________________________ *)
 
 val type_check:
-   (BrgType.message -> 'a) -> (Brg.term option -> Brg.unit -> 'a) -> 
-   ?si:bool -> Hierarchy.graph -> Brg.unit -> 'a
+   (BrgType.message -> 'a) -> (Brg.term option -> Brg.entity -> 'a) -> 
+   ?si:bool -> Hierarchy.graph -> Brg.entity -> 'a
diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make
index ccf9cfd65..8085aa65b 100644
--- a/helm/software/lambda-delta/common/Make
+++ b/helm/software/lambda-delta/common/Make
@@ -1 +1 @@
-hierarchy output unit library
+hierarchy output entity library
diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml
new file mode 100644
index 000000000..78d7c3ace
--- /dev/null
+++ b/helm/software/lambda-delta/common/entity.ml
@@ -0,0 +1,17 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+type uri = NUri.uri
+type id = Aut.id
+
+type 'bind entry = int * uri * 'bind (* age, uri, binder *)
+
+type 'bind entity = 'bind entry option
diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml
index c60a227e7..8ef875ce7 100644
--- a/helm/software/lambda-delta/common/library.ml
+++ b/helm/software/lambda-delta/common/library.ml
@@ -42,7 +42,7 @@ let close_entry frm =
 
 (* interface functions ******************************************************)
 
-let export_unit export_entry si g = function
+let export_entity export_entry si g = function
    | Some entry ->
       let _, uri, bind = entry in
       let path = path_of_uri uri in
diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli
index 1a10b6e9d..68325f3d9 100644
--- a/helm/software/lambda-delta/common/library.mli
+++ b/helm/software/lambda-delta/common/library.mli
@@ -9,6 +9,6 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val export_unit:
-   (Format.formatter -> 'bind Unit.entry -> unit) -> 
-   bool -> Hierarchy.graph -> 'bind Unit.unit -> unit
+val export_entity:
+   (Format.formatter -> 'bind Entity.entry -> unit) -> 
+   bool -> Hierarchy.graph -> 'bind Entity.entity -> unit
diff --git a/helm/software/lambda-delta/common/unit.ml b/helm/software/lambda-delta/common/unit.ml
deleted file mode 100644
index d76b9d9fe..000000000
--- a/helm/software/lambda-delta/common/unit.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-type uri = NUri.uri
-type id = Aut.id
-
-type 'bind entry = int * uri * 'bind (* age, uri, binder *)
-
-type 'bind unit = 'bind entry option
diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml
index a3cb08585..563e19b99 100644
--- a/helm/software/lambda-delta/toplevel/meta.ml
+++ b/helm/software/lambda-delta/toplevel/meta.ml
@@ -9,19 +9,19 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-type uri = Unit.uri
+type uri = Entity.uri
 
-type id = Unit.id
+type id = Entity.id
 
 type term = Sort of bool                  (* sorts: true = TYPE, false = PROP *)
 	  | LRef of int * int             (* local reference: local environment length, de bruijn index *)
 	  | GRef of int * uri * term list (* global reference: local environment length, name, arguments *)
 	  | Appl of term * term           (* application: argument, function *)
-	  | Abst of id * term * term      (* abstraction: name, type, scope *)
+	  | Abst of id * term * term      (* abstraction: name, domain, scope *)
 
 type pars = (id * term) list (* parameter declarations: name, type *)
 
-(* entry: line number, parameters, name, type, (transparent?, body) *)
+(* entry: line number, parameters, name, domain, (transparent?, body) *)
 type entry = int * pars * uri * term * (bool * term) option
 
-type unit = entry option
+type entity = entry option
diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 335f57fc0..db18ade47 100644
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -145,7 +145,7 @@ let rec xlate_term f st lenv = function
       in
       resolve_lref f st l lenv (id_of_name name)
 
-let xlate_unit f st = function
+let xlate_entity f st = function
    | A.Section (Some (_, name))     ->
       f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
    | A.Section None            ->
@@ -204,4 +204,4 @@ let xlate_unit f st = function
 let initial_status ?(cover="") () =
    initial_status hsize cover
 
-let meta_of_aut = xlate_unit
+let meta_of_aut = xlate_entity
diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli
index 79c8fb22b..cfcb49d0b 100644
--- a/helm/software/lambda-delta/toplevel/metaAut.mli
+++ b/helm/software/lambda-delta/toplevel/metaAut.mli
@@ -13,4 +13,4 @@ type status
 
 val initial_status: ?cover:string -> unit -> status 
 
-val meta_of_aut: (status -> Meta.unit -> 'a) -> status -> Aut.unit -> 'a
+val meta_of_aut: (status -> Meta.entity -> 'a) -> status -> Aut.entity -> 'a
diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml
index 89c1527c8..67c938df0 100644
--- a/helm/software/lambda-delta/toplevel/metaBag.ml
+++ b/helm/software/lambda-delta/toplevel/metaBag.ml
@@ -63,10 +63,10 @@ let xlate_entry f = function
       let f c = unwind_to_xlate_term (f c) c u in
       xlate_pars f pars
 
-let xlate_unit f = function
+let xlate_entity f = function
    | None   -> f None
    | Some e -> let f e = f (Some e) in xlate_entry f e
 
 (* Interface functions ******************************************************)
 
-let bag_of_meta = xlate_unit
+let bag_of_meta = xlate_entity
diff --git a/helm/software/lambda-delta/toplevel/metaBag.mli b/helm/software/lambda-delta/toplevel/metaBag.mli
index f19f6dd76..b8e41be04 100644
--- a/helm/software/lambda-delta/toplevel/metaBag.mli
+++ b/helm/software/lambda-delta/toplevel/metaBag.mli
@@ -9,4 +9,4 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val bag_of_meta: (Bag.unit -> 'a) -> Meta.unit -> 'a
+val bag_of_meta: (Bag.entity -> 'a) -> Meta.entity -> 'a
diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml
index eff9e9c55..2fb17262e 100644
--- a/helm/software/lambda-delta/toplevel/metaBrg.ml
+++ b/helm/software/lambda-delta/toplevel/metaBrg.ml
@@ -62,10 +62,10 @@ let xlate_entry f = function
       let f c = unwind_to_xlate_term (f c) c u in
       xlate_pars f pars
 
-let xlate_unit f = function
+let xlate_entity f = function
    | None   -> f None
    | Some e -> let f e = f (Some e) in xlate_entry f e
 
 (* Interface functions ******************************************************)
 
-let brg_of_meta = xlate_unit
+let brg_of_meta = xlate_entity
diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli
index b07ed1253..6a4a7bd2b 100644
--- a/helm/software/lambda-delta/toplevel/metaBrg.mli
+++ b/helm/software/lambda-delta/toplevel/metaBrg.mli
@@ -9,4 +9,4 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val brg_of_meta: (Brg.unit -> 'a) -> Meta.unit -> 'a
+val brg_of_meta: (Brg.entity -> 'a) -> Meta.entity -> 'a
diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.ml b/helm/software/lambda-delta/toplevel/metaLibrary.ml
index a6e780a5f..3ae116d96 100644
--- a/helm/software/lambda-delta/toplevel/metaLibrary.ml
+++ b/helm/software/lambda-delta/toplevel/metaLibrary.ml
@@ -29,8 +29,8 @@ let open_out f name =
    F.pp_set_margin frm max_int;
    f (och, frm)
 
-let write_unit f (_, frm) unit =
-   O.pp_unit f frm unit
+let write_entity f (_, frm) entity =
+   O.pp_entity f frm entity
    
 let close_out f (och, _) =
    close_out och; f ()
diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.mli b/helm/software/lambda-delta/toplevel/metaLibrary.mli
index 26172e46c..2f6e41b80 100644
--- a/helm/software/lambda-delta/toplevel/metaLibrary.mli
+++ b/helm/software/lambda-delta/toplevel/metaLibrary.mli
@@ -13,6 +13,6 @@ type out_channel
 
 val open_out: (out_channel -> 'a) -> string -> 'a
 
-val write_unit: (unit -> 'a) -> out_channel -> Meta.unit -> 'a
+val write_entity: (unit -> 'a) -> out_channel -> Meta.entity -> 'a
 
 val close_out: (unit -> 'a) -> out_channel -> 'a
diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml
index a8560ab18..7f62c8abc 100644
--- a/helm/software/lambda-delta/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/toplevel/metaOutput.ml
@@ -77,7 +77,7 @@ let count_entry f c = function
       let f c = count_term f c w in
       Cps.list_fold_left f count_par c pars
 
-let count_unit f c = function
+let count_entity f c = function
    | Some e -> count_entry f c e
    | None   -> f c
 
@@ -150,6 +150,6 @@ let pp_entry frm (l, pars, uri, u, body) =
    F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
       l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u
 
-let pp_unit f frm = function 
+let pp_entity f frm = function 
    | Some entry -> pp_entry frm entry; f ()
    | None       -> f ()
diff --git a/helm/software/lambda-delta/toplevel/metaOutput.mli b/helm/software/lambda-delta/toplevel/metaOutput.mli
index 611e12139..1a7b119ce 100644
--- a/helm/software/lambda-delta/toplevel/metaOutput.mli
+++ b/helm/software/lambda-delta/toplevel/metaOutput.mli
@@ -13,8 +13,8 @@ type counters
 
 val initial_counters: counters
 
-val count_unit: (counters -> 'a) -> counters -> Meta.unit -> 'a
+val count_entity: (counters -> 'a) -> counters -> Meta.entity -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
-val pp_unit: (unit -> 'a) -> Format.formatter -> Meta.unit -> 'a
+val pp_entity: (unit -> 'a) -> Format.formatter -> Meta.entity -> 'a
diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index e87bf8a07..c3923b387 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -49,8 +49,8 @@ let initial_status cover = {
    ast  = AP.initial_status
 }
 
-let count count_fun c unit =
-   if !L.level > 2 then count_fun C.start c unit else c
+let count count_fun c entity =
+   if !L.level > 2 then count_fun C.start c entity else c
 
 let flush () = L.flush 0; L.flush_err ()
 
@@ -60,16 +60,16 @@ let bag_error s msg =
 let brg_error s msg =
    L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush () 
 
-let process_unit f st =
+let process_entity f st =
    let f ast = f {st with ast = ast} in
-   AP.process_unit f st.ast
+   AP.process_entity f st.ast
 
 (* kernel related ***********************************************************)
 
 type kernel = Brg | Bag
 
-type kernel_unit = Brgunit of Brg.unit
-                 | Bagunit of Bag.unit
+type kernel_entity = BrgEntity of Brg.entity
+                   | BagEntity of Bag.entity
 
 let kernel = ref Brg
 
@@ -77,21 +77,21 @@ let print_counters st = match !kernel with
    | Brg -> BrgO.print_counters C.start st.brgc
    | Bag -> BagO.print_counters C.start st.bagc
 
-let kernel_of_meta f st unit = match !kernel with
+let kernel_of_meta f st entity = match !kernel with
    | Brg -> 
-      let f unit = f st (Brgunit unit) in
-      MBrg.brg_of_meta f unit
+      let f entity = f st (BrgEntity entity) in
+      MBrg.brg_of_meta f entity
    | Bag -> 
-      let f unit = f st (Bagunit unit) in
-      MBag.bag_of_meta f unit  
+      let f entity = f st (BagEntity entity) in
+      MBag.bag_of_meta f entity  
 
-let count_unit st = function
-   | Brgunit unit -> {st with brgc = count BrgO.count_unit st.brgc unit}
-   | Bagunit unit -> {st with bagc = count BagO.count_unit st.bagc unit}
+let count_entity st = function
+   | BrgEntity entity -> {st with brgc = count BrgO.count_entity st.brgc entity}
+   | BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity}
 
-let export_unit si g = function
-   | Brgunit unit -> G.export_unit BrgO.export_entry si g unit
-   | Bagunit _    -> ()
+let export_entity si g = function
+   | BrgEntity entity -> G.export_entity BrgO.export_entry si g entity
+   | BagEntity _    -> ()
 
 let type_check f st si g k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
@@ -100,8 +100,8 @@ let type_check f st si g k =
       | Some (i, u, _) -> f st (Some (i, u))
    in
    match k with
-      | Brgunit unit -> BrgU.type_check brg_err f ~si g unit
-      | Bagunit unit -> BagU.type_check f ~si g unit
+      | BrgEntity entity -> BrgU.type_check brg_err f ~si g entity
+      | BagEntity entity -> BagU.type_check f ~si g entity
 
 (****************************************************************************)
 
@@ -152,7 +152,7 @@ try
       if !L.level > 0 then T.utime_stamp "parsed";
       let rec aux st = function
          | []         -> st
-	 | unit :: tl ->
+	 | entity :: tl ->
 (* stage 3 *)
 	    let f st = function
 	       | None        -> st
@@ -162,31 +162,31 @@ try
 		  st
 	    in
 (* stage 2 *)	    
-	    let f st unit =
-	       let st = count_unit st unit in
-	       if !export then export_unit !si !graph unit;
-	       if !stage > 2 then type_check f st !si !graph unit else st
+	    let f st entity =
+	       let st = count_entity st entity in
+	       if !export then export_entity !si !graph entity;
+	       if !stage > 2 then type_check f st !si !graph entity else st
 	    in
 (* stage 1 *)	    
-	    let f st mst unit = 
+	    let f st mst entity = 
 	       let st = {st with
-	          mst = mst; mc = count MO.count_unit st.mc unit
+	          mst = mst; mc = count MO.count_entity st.mc entity
 	       } in
 	       begin match !moch with
 	          | None     -> ()
-		  | Some och -> ML.write_unit C.start och unit
+		  | Some och -> ML.write_entity C.start och entity
 	       end;
-	       if !stage > 1 then kernel_of_meta f st unit else st 
+	       if !stage > 1 then kernel_of_meta f st entity else st 
 	    in  
 (* stage 0 *)	    
-            let st = {st with ac = count AO.count_unit st.ac unit} in
-	    let f st unit =
+            let st = {st with ac = count AO.count_entity st.ac entity} in
+	    let f st entity =
 	       let st = 
-	          if !stage > 0 then MA.meta_of_aut (f st) st.mst unit else st
+	          if !stage > 0 then MA.meta_of_aut (f st) st.mst entity else st
 	       in
 	       aux st tl
 	    in
-	    if !process then process_unit f st unit else f st unit
+	    if !process then process_entity f st entity else f st entity
       in
       O.clear_reductions ();
       let cover = if !use_cover then base_name else "" in