]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgUntrusted.ml
- simpler attribute system
[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml
index 877fee9d8380e6f739d237ed385660a3e446bfb7..d6333552f59e520a85075b2b3200afa64b7fff18 100644 (file)
@@ -33,7 +33,7 @@ let type_check err f st = function
       let f xt tt = 
          let xt = match xt with
            | B.Cast _ -> xt
-           | _        -> B.Cast (E.empty_node, tt, xt)
+           | _        -> B.Cast (tt, xt)
         in
          let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
       in
@@ -44,7 +44,7 @@ let validate err f st e =
    let uri, t = match e with
       | _, _, uri, E.Abst t -> uri, t
       | _, _, uri, E.Abbr t -> uri, t
-      | _, _, _,    E.Void   -> assert false
+      | _, _, _,   E.Void   -> assert false
    in
    let err msg = err (L.Uri uri :: msg) in
    let f () = let _ = BE.set_entity e in f () in