]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_ag/bagUntrusted.ml
new message reporting system improves performance significatively
[helm.git] / helm / software / helena / src / basic_ag / bagUntrusted.ml
index 5d04a3bf47d4e35af5f141f93ba8a5dc1e565d66..c27ec5ed1d94e1c8f0f51fa6f4db44009b798cc8 100644 (file)
@@ -19,11 +19,13 @@ module ZT = BagType
 (* Interface functions ******************************************************)
 
 (* to share *)
-let type_check f st = function
+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 = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in
-      L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t
+      ZT.type_of err f st Z.empty_lenv t
    | a, uri, E.Abbr t      ->
+      let err msg = err (L.Uri uri :: msg) in
       let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in
-      L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t
+      ZT.type_of err f st Z.empty_lenv t
    | _, _, E.Void          -> assert false