X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgType.ml;h=2bead2d3344b3237f96ad71c6c5cc048cb1c5cdb;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=5515e4404759f24793a5e45083f43904a361353a;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml
index 5515e4404..2bead2d33 100644
--- a/helm/software/lambda-delta/src/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgType.ml
@@ -15,6 +15,7 @@ module S  = Share
 module L  = Log
 module H  = Hierarchy
 module E  = Entity
+module N  = Level
 module B  = Brg
 module BE = BrgEnvironment
 module BS = BrgSubstitution
@@ -55,11 +56,12 @@ let assert_convertibility err f st m u w v =
 
 let assert_applicability err f st m u w v =
    match BR.xwhd st m u with 
-      | _, B.Sort _                 -> error1 err "not a function type" m u
-      | mu, B.Bind (_, B.Abst u, _) -> 
+      | _, B.Sort _                      ->
+         error1 err "not a function type" m u
+      | mu, B.Bind (_, B.Abst (_, u), _) -> 
          if BR.are_convertible st mu u m w then f () else
 	 error3 err m v w ~mu u
-      | _                         -> assert false (**)
+      | _                                -> assert false (**)
 
 let rec b_type_of err f st m x =
    log1 "Now checking" m x;
@@ -68,7 +70,7 @@ let rec b_type_of err f st m x =
       let h = H.apply h in f x (B.Sort (a, h)) 
    | B.LRef (_, i)           ->
       begin match BR.get m i with
-         | B.Abst w                  ->
+         | B.Abst (_, w)     ->
 	    f x (BS.lift (succ i) (0) w)
 	 | B.Abbr (B.Cast (_, w, _)) -> 
 	    f x (BS.lift (succ i) (0) w)
@@ -78,7 +80,7 @@ let rec b_type_of err f st m x =
       end
    | B.GRef (_, uri)         ->
       begin match BE.get_entity uri with
-         | _, _, E.Abst w                  -> f x w
+         | _, _, E.Abst (_, w)             -> f x w
 	 | _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
 	 | _, _, E.Abbr _                  -> assert false
 	 | _, _, E.Void                    ->
@@ -95,12 +97,12 @@ let rec b_type_of err f st m x =
          | _        -> f (B.Cast ([], vv, xv))
       in
       type_of err f st m v
-   | B.Bind (a, B.Abst u, t) ->
+   | B.Bind (a, B.Abst (n, 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 (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) 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 xu)) 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 =