the sort hierarchy parameter enter the kernel status

[helm.git] / helm / software / lambda-delta / common / entity.ml

diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml
index 5bef9ff3347524351d62eac91e5cd4c340a5afa1..d6314150b935e77fca6d6bedbeb7a58c04548cbb 100644 (file)
--- 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
 }