update in helena

[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 431e3e4737f3676452aae3fb5e74d9d287e8fc2c..28a2755481a6e750b577d95c8ecbbe4680a50232 100644 (file)
--- 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