- siimplifified RTM (one register less) now counts x-steps.

[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 d028e058527d8bc08ecfd0aa9b94650e8941eebc..ad4154fc17241316160c8405211210d7471720ee 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -53,9 +53,9 @@ let assert_convertibility err f st m u t =
 let assert_applicability err f st m v t =
    if !G.trace >= level then warn "Asserting applicability";
    match BR.xwhd st m None t with 
-      | _, B.Sort _                      ->
+      | _, B.Sort _                            ->
          error1 err "not a function" m t
-      | mw, B.Bind (_, B.Abst (n, w), _) ->
+      | mw, B.Bind (_, B.Abst (true, n, w), _) ->
          if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t
          else begin
             if !G.trace >= level then warn "Asserting convertibility for application";
@@ -85,9 +85,9 @@ let rec b_validate err f st m x =
    | B.Bind (a, b, t) ->
       let f () = b_validate err f st (BR.push m a b) t in
       begin match b with 
-         | B.Abst (n, u) -> validate err f st m u
-         | B.Abbr v      -> validate err f st m v
-         | B.Void        -> f ()
+         | B.Abst (_, n, u) -> validate err f st m u
+         | B.Abbr v         -> validate err f st m v
+         | B.Void           -> f ()
       end
    | B.Appl (_, v, t)        ->
       let f () = assert_applicability err f st m v t in