the sort hierarchy parameter enter the kernel status

[helm.git] / helm / software / lambda-delta / basic_rg / brgType.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index 728e3ff416e75c0e2322b65c65b11fa1a2cc4a24..8443cd16602aa7c75645a4c41e480d81a4f37e8f 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -62,11 +62,11 @@ let assert_applicability err f st m u w v =
         error3 err m v w ~mu u
       | _                         -> assert false (**)
 
-let rec b_type_of err f st g m x =
+let rec b_type_of err f st m x =
    log1 "Now checking" m x;
    match x with
    | B.Sort (a, h)           ->
-      let h = H.apply g h in f x (B.Sort (a, h)) 
+      let h = H.apply st.Y.g h in f x (B.Sort (a, h)) 
    | B.LRef (_, i)           ->
       begin match R.get m i with
          | B.Abst w                  ->
@@ -89,43 +89,43 @@ let rec b_type_of err f st g m x =
       let f xv xt tt =
          f (A.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 g m t in
+      let f xv m = b_type_of err (f xv) st m t in
       let f xv = f xv (R.push m a (B.abbr xv)) in
       let f xv vv = match xv with 
         | B.Cast _ -> f xv
          | _        -> f (B.Cast ([], vv, xv))
       in
-      type_of err f st g m v
+      type_of err f st m v
    | B.Bind (a, B.Abst u, t) ->
       let f xu xt tt =
         f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
       in
-      let f xu m = b_type_of err (f xu) st g m t in
+      let f xu m = b_type_of err (f xu) st m t in
       let f xu _ = f xu (R.push m a (B.abst xu)) in
-      type_of err f st g m u
+      type_of err f st m u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
          f (A.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
       in
-      b_type_of err f st g (R.push m a B.Void) t
+      b_type_of err f st (R.push m a B.Void) t
          
    | B.Appl (a, v, t)        ->
       let f xv vv xt tt = 
          let f _ = f (A.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 g m t in
-      type_of err f st g m v
+      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 (A.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 g m t in
-      type_of err f st g m u
+      let f xu _ = b_type_of err (f xu) st m t in
+      type_of err f st m u
 
 (* Interface functions ******************************************************)
 
-and type_of err f st g m x =
+and type_of err f st m x =
    let f t u = L.unbox level; f t u in
-   L.box level; b_type_of err f st g m x
+   L.box level; b_type_of err f st m x