X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgUntrusted.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgUntrusted.ml;h=4c1ae61dbc47cfd6cd40220d5832c4e95201f15e;hb=93205dc852fa208b48a05757d05d9910b7d45fa1;hp=311061aaac2866061008041d6507b00ee182855c;hpb=201283b23b8aa4d55cfe4e1dc19c24057803f2e0;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 311061aaa..4c1ae61db 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -28,6 +28,10 @@ let type_check err f st = function L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t | a, uri, Y.Abbr t -> let f xt tt = + let xt = match xt with + | B.Cast _ -> xt + | _ -> B.Cast ([], tt, xt) + in let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e in L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t