X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgValidity.ml;h=a1401c125a1a01c114daeac350170b88a0c80288;hp=cb0fc4060c69f6e41cf734f8b38bbe5fd97b4b52;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hpb=fdb80b08af83b86759833142456ce3c4f84cd80e

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index cb0fc4060..a1401c125 100644
--- 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)          ->