X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgType.ml;h=4bf5882a4885a48cf53e1fc4af257e875820bc9e;hb=448920d42f3f7886d27477281b22f0c11771d4ed;hp=8c9996c22a3fbb000cd3a8f7d8717606052bf733;hpb=dcdee4ca839dac671924a95f0ada71faf06a8be4;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index 8c9996c22..4bf5882a4 100644
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -11,12 +11,13 @@
 
 module U = NUri
 module C = Cps
-module S = Share
+module A = Share
 module L = Log
 module H = Hierarchy
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
+module S = BrgSubstitution
 module R = BrgReduction
 
 exception TypeError of B.message
@@ -51,8 +52,10 @@ let rec b_type_of f g c x =
       let f h = f x (B.Sort (a, h)) in H.apply f g h
    | B.LRef (_, i)           ->
       let f _ = function
-         | Some (_, B.Abst w)                  -> f x w
-	 | Some (_, B.Abbr (B.Cast (_, w, _))) -> f x w
+         | Some (_, B.Abst w)                  ->
+	    S.lift (f x) (succ i) (0) w
+	 | Some (_, B.Abbr (B.Cast (_, w, _))) -> 
+	    S.lift (f x) (succ i) (0) w
 	 | Some (_, B.Abbr _)                  -> assert false
 	 | Some (_, B.Void)                    -> 
 	    error1 "reference to excluded variable" c x
@@ -71,7 +74,7 @@ let rec b_type_of f g c x =
       E.get_obj f uri   
    | B.Bind (a, B.Abbr v, t) ->
       let f xv xt tt =
-         f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+         f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
       in
       let f xv cc = b_type_of (f xv) g cc t in
       let f xv = B.push (f xv) c a (B.Abbr xv) in
@@ -82,14 +85,14 @@ let rec b_type_of f g c x =
       type_of f g c v
    | B.Bind (a, B.Abst u, t) ->
       let f xu xt tt =
-	 f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
+	 f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
       in
       let f xu cc = b_type_of (f xu) g cc t in
       let f xu _ = B.push (f xu) c a (B.Abst xu) in
       type_of f g c u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
-         f (S.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
+         f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
       in
       let f cc = b_type_of f g cc t in
       B.push f c a B.Void   
@@ -101,7 +104,7 @@ let rec b_type_of f g c x =
 	    L.unbox (succ level);
 	    let f r =
 (*	       L.warn (Printf.sprintf "Convertible: %b" a); *)
-	       if r then f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt)
+	       if r then f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt)
 	       else error3 c xv vv w
 	    in
 	    R.are_convertible f ~si:!si c w vv
@@ -114,7 +117,7 @@ let rec b_type_of f g c x =
    | B.Cast (a, u, t)        ->
       let f xu xt tt r =  
          (* L.warn (Printf.sprintf "Convertible: %b" a); *)
-	 if r then f (S.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu
+	 if r then f (A.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu
       in
       let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) c xu tt in
       let f xu _ = b_type_of (f xu) g c t in