X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcommon%2Fentity.ml;h=d6314150b935e77fca6d6bedbeb7a58c04548cbb;hb=0920a5755553774f5b41d7603318ea997ecbdca5;hp=5bef9ff3347524351d62eac91e5cd4c340a5afa1;hpb=2e451dca46e509fd7e7772f3d2e438c189ce10a1;p=helm.git

diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml
index 5bef9ff33..d6314150b 100644
--- a/helm/software/lambda-delta/common/entity.ml
+++ b/helm/software/lambda-delta/common/entity.ml
@@ -28,9 +28,11 @@ type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
 type uri_generator = string -> string
 
 type status = {
-   delta: bool; (* global delta-expansion *)
-   rt: bool;    (* reference typing *)
-   si: bool     (* sort inclusion *)
+   g: Hierarchy.graph; (* sort hierarchy parameter *)
+   delta: bool;        (* global delta-expansion *)
+   rt: bool;           (* reference typing *)
+   si: bool;           (* sort inclusion *)
+   expand: bool        (* always expand global definitions *)
 }
 
 (* helpers ******************************************************************)
@@ -94,6 +96,6 @@ let xlate f xlate_term = function
    | _, _, Void   ->
       assert false
 
-let initial_status si = {
-   delta = false; rt = false; si = si
+let initial_status g expand si = {
+   g = g; delta = false; rt = false; si = si; expand = expand
 }