- we are moving from old (patched) management of sort inclusion

[helm.git] / helm / software / helena / src / toplevel / top.ml

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index 535450c1f155d7b6a2a556818833eaa6e77c0d10..bded35b3bc126ed1fd547678203a717c8d7a275d 100644 (file)
--- a/helm/software/helena/src/toplevel/top.ml
+++ b/helm/software/helena/src/toplevel/top.ml
@@ -18,9 +18,9 @@ module L  = Log
 module Y  = Time
 module G  = Options
 module H  = Hierarchy
+module N  = Layer
 module E  = Entity
 module O  = Output
-module S  = Status
 module DO = CrgOutput
 module TD = TxtCrg
 module AA = AutProcess
@@ -39,7 +39,7 @@ module ZT = BagType
 module ZU = BagUntrusted
 
 type status = {
-   kst: S.status;
+   kst: N.status;
    tst: TD.status;
    pst: AA.status;
    ast: AD.status;
@@ -53,13 +53,13 @@ type status = {
 let level = 0
 
 let bag_error st s msg =
-   L.error st.kst.S.lenv ZO.specs (L.Warn s :: msg) 
+   L.error st.kst ZO.specs (L.Warn s :: msg) 
 
 let brg_error st s msg =
-   L.error st.kst.S.lenv BR.specs (L.Warn s :: msg)
+   L.error st.kst BR.specs (L.Warn s :: msg)
 
 let initial_status () = {
-   kst = S.initial_status ();
+   kst = N.initial_status ();
    tst = TD.initial_status ();
    pst = AA.initial_status ();
    ast = AD.initial_status ();
@@ -71,7 +71,7 @@ let initial_status () = {
 }
 
 let refresh_status st = {st with
-   kst = S.refresh_status st.kst;
+   kst = N.refresh_status st.kst;
    tst = TD.refresh_status st.tst;
    ast = AD.refresh_status st.ast;
 }
@@ -91,7 +91,7 @@ let xlate_entity st entity = match !G.kernel, entity with
    | G.Brg, CrgEntity e -> 
       let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
    | G.Bag, CrgEntity e -> 
-      let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst.S.lenv) e
+      let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e
    | _, entity          -> entity
 
 let pp_progress e =
@@ -110,9 +110,9 @@ let count_entity st = function
    | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
 
 let export_entity st = function
-   | CrgEntity e -> XL.export_entity (XD.export_term st.kst.S.lenv) e
-   | BrgEntity e -> XL.export_entity (BO.export_term st.kst.S.lenv) e
-   | BagEntity e -> XL.export_entity (ZO.export_term st.kst.S.lenv) e
+   | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e
+   | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e
+   | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e
 
 let type_check st k =
    let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in
@@ -132,7 +132,7 @@ let validate st k =
          begin match st.och with
             | None     -> st
             | Some och -> 
-               if BG.output_entity st.kst.S.lenv och entity then st
+               if BG.output_entity st.kst och entity then st
                else begin L.warn level "Matita exportation stopped"; {st with och = None} end
          end
       | BagEntity _      -> st