]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgUntrusted.ml
new message reporting system improves performance significatively
[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml
index 373f9497399622582a6267c54411ff59fed53fde..88edd46d8dee15f0a559da19014ac33653fdd6e6 100644 (file)
@@ -23,11 +23,13 @@ module BV = BrgValidity
 (* to share *)
 let type_check err f st = function
    | a, uri, E.Abst (n, t) ->
+      let err msg = err (L.Uri uri :: msg) in
       let f xt tt = 
          let e = BE.set_entity (a, uri, E.Abst (n, xt)) in f tt e
       in
-      L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
+      BT.type_of err f st BR.empty_kam t
    | a, uri, E.Abbr t      ->
+      let err msg = err (L.Uri uri :: msg) in
       let f xt tt = 
          let xt = match xt with
            | B.Cast _ -> xt
@@ -35,7 +37,7 @@ let type_check err f st = function
         in
          let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e
       in
-      L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
+      BT.type_of err f st BR.empty_kam t
    | _, _, E.Void          -> assert false
 
 let validate err f st e =
@@ -44,5 +46,6 @@ let validate err f st e =
       | _, uri, E.Abbr t      -> uri, t
       | _, _,   E.Void        -> assert false
    in
+   let err msg = err (L.Uri uri :: msg) in
    let f () = let _ = BE.set_entity e in f () in
-   L.loc := U.string_of_uri uri; BV.validate err f st BR.empty_kam t
+   BV.validate err f st BR.empty_kam t