update in helena

[helm.git] / helm / software / helena / src / basic_rg / brgValidity.ml

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index cb0fc4060c69f6e41cf734f8b38bbe5fd97b4b52..a1401c125a1a01c114daeac350170b88a0c80288 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -52,8 +52,8 @@ ELSE () END;
    if BR.are_convertible st m zero u m one t then f () else
    error2 err m u m t
 
-let assert_applicability err f st m x v t =
-   let mode, msg = if x then None, "extended" else one, "restricted" in 
+let assert_applicability err f st m a v t =
+   let mode, msg = if a.E.a_rest then one, "restricted" else None, "extended" in 
 IFDEF TRACE THEN
    if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability")
 ELSE () END;
@@ -98,8 +98,8 @@ ELSE () END;
          | B.Abbr v         -> validate err f st m v
          | B.Void           -> f ()
       end
-   | B.Appl (x, v, t)       ->
-      let f () = assert_applicability err f st m x v t in
+   | B.Appl (a, v, t)       ->
+      let f () = assert_applicability err f st m a v t in
       let f () = b_validate err f st m t in
       validate err f st m v
    | B.Cast (u, t)          ->