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

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index 5de70fbfa..a1401c125 100644
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -46,18 +46,24 @@ let zero = Some 0
 let one = Some 1
 
 let assert_convertibility err f st m u t =
-   if !G.ct >= level then warn "Asserting convertibility for cast";
+IFDEF TRACE THEN
+   if !G.ct >= level then warn "Asserting convertibility for cast"
+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 
-   if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability");
+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;
    match BR.xwhd st m mode t with 
       | 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.ct >= level then warn "Asserting convertibility for application";
+IFDEF TRACE THEN
+            if !G.ct >= level then warn "Asserting convertibility for application"
+ELSE () END;
             if BR.are_convertible st mw zero w m one v then f () else
 	    error2 err mw w m v
          end
@@ -66,7 +72,9 @@ let assert_applicability err f st m x v t =
       | _                                      -> assert false (**)
 
 let rec b_validate err f st m y =
-   if !G.ct >= level then log1 st "Now checking" m y;
+IFDEF TRACE THEN
+   if !G.ct >= level then log1 st "Now checking" m y
+ELSE () END;
    match y with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->
@@ -90,8 +98,8 @@ let rec b_validate err f st m y =
          | 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)          ->