X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgType.ml;h=28a2755481a6e750b577d95c8ecbbe4680a50232;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=431e3e4737f3676452aae3fb5e74d9d287e8fc2c;hpb=586c361209ac14e8c2b1da3509041c0c82a86c92;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 431e3e473..28a275548 100644
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -57,8 +57,8 @@ let assert_convertibility err f st m u w v =
    if BR.are_convertible st m zero u m zero w then f () else
    error3 err m v w u
 
-let assert_applicability err f st m x u w v =
-   let mode = if x then None else zero in
+let assert_applicability err f st m a u w v =
+   let mode = if a.E.a_rest then zero else None in
    match BR.xwhd st m mode u with 
       | _, B.Sort _                            ->
          error1 err "not a function type" m u
@@ -87,10 +87,10 @@ ELSE () END;
       end
    | B.GRef (_, u)                   ->
       begin match BE.get_entity u with
-         | _, _, _, E.Abst w               -> f z w
-	 | _, _, _, E.Abbr (B.Cast (w, _)) -> f z w
-	 | _, _, _, E.Abbr _               -> assert false
-	 | _, _, _, E.Void                 ->
+         | _, _, _, E.Abst (_, w)             -> f z w
+	 | _, _, _, E.Abbr (_, B.Cast (w, _)) -> f z w
+	 | _, _, _, E.Abbr _                  -> assert false
+	 | _, _, _, E.Void                    ->
             error1 err "reference to unknown entry" m z
       end
    | B.Bind (y, B.Abbr v, t)         ->
@@ -116,10 +116,10 @@ ELSE () END;
          f (S.sh1 t rt z (B.bind_void y)) (B.bind_void y tt)
       in
       b_type_of err f st (BR.push m y B.Void) t
-   | B.Appl (x, v, t)                ->
+   | B.Appl (a, v, t)                ->
       let f rv vv rt tt = 
-         let f _ = f (S.sh2 v rv t rt z (B.appl x)) (B.appl x rv tt) in
-         assert_applicability err f st m x tt vv rv
+         let f _ = f (S.sh2 v rv t rt z (B.appl a)) (B.appl a rv tt) in
+         assert_applicability err f st m a tt vv rv
       in
       let f rv vv = b_type_of err (f rv vv) st m t in
       type_of err f st m v