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

[helm.git] / helm / software / helena / src / basic_rg / brgType.ml

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 85a20cbc0e6b4c7e7ea9c2ecb2293692dc464f6a..2dfb2552dc375649f8c8e0f3fc6ebb7a82a021d8 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -11,13 +11,12 @@
 
 module U  = NUri
 module C  = Cps
-module W  = Share
+module S  = Share
 module L  = Log
 module G  = Options
 module H  = Hierarchy
-module N  = Level
+module N  = Layer
 module E  = Entity
-module S  = Status
 module B  = Brg
 module BE = BrgEnvironment
 module BS = BrgSubstitution
@@ -66,7 +65,7 @@ let assert_applicability err f st m u w v =
       | _                                -> assert false (**)
 
 let rec b_type_of err f st m x =
-   if !G.trace >= level then log1 st.S.lenv "Now checking" m x;
+   if !G.trace >= level then log1 st "Now checking" m x;
    match x with
    | B.Sort (a, h)           ->
       let h = H.apply h in f x (B.Sort (a, h)) 
@@ -90,7 +89,7 @@ let rec b_type_of err f st m x =
       end
    | B.Bind (a, B.Abbr v, t) ->
       let f xv xt tt =
-         f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+         f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
       in
       let f xv m = b_type_of err (f xv) st m t in
       let f xv = f xv (BR.push m a (B.abbr xv)) in
@@ -101,27 +100,27 @@ let rec b_type_of err f st m x =
       type_of err f st m v
    | B.Bind (a, B.Abst (n, u), t) ->
       let f xu xt tt =
-        f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st.S.lenv n 1) a xu tt)
+        f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st n 1) a xu tt)
       in
       let f xu m = b_type_of err (f xu) st m t in
       let f xu _ = f xu (BR.push m a (B.abst n xu)) in
       type_of err f st m u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
-         f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+         f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
       in
       b_type_of err f st (BR.push m a B.Void) t
          
    | B.Appl (a, v, t)        ->
       let f xv vv xt tt = 
-         let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+         let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
          assert_applicability err f st m tt vv xv
       in
       let f xv vv = b_type_of err (f xv vv) st m t in
       type_of err f st m v
    | B.Cast (a, u, t)        ->
       let f xu xt tt =  
-        let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in
+        let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in
          assert_convertibility err f st m xu tt xt
       in
       let f xu _ = b_type_of err (f xu) st m t in