]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgUntrusted.ml
- we removed a flag from the kernel status
[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml
index 87a3f60cfff3942573016435c7466cc5597235f2..8425774d2a6bc890cb4cd439b67fec74ee9ab24c 100644 (file)
@@ -27,7 +27,7 @@ let type_check err f st = function
       let f xt tt = 
          let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e
       in
-      BT.type_of err f st BR.empty_kam t
+      BT.type_of err f st BR.empty_rtm t
    | ra, na, uri, E.Abbr t ->
       let err msg = err (L.Uri uri :: msg) in
       let f xt tt = 
@@ -37,7 +37,7 @@ let type_check err f st = function
         in
          let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
       in
-      BT.type_of err f st BR.empty_kam t
+      BT.type_of err f st BR.empty_rtm t
    | _, _, _, E.Void       -> assert false
 
 let validate err f st e =
@@ -48,4 +48,4 @@ let validate err f st e =
    in
    let err msg = err (L.Uri uri :: msg) in
    let f () = let _ = BE.set_entity e in f () in
-   BV.validate err f st BR.empty_kam t
+   BV.validate err f st BR.empty_rtm t