]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgUntrusted.ml
- new attributes system
[helm.git] / helm / software / helena / src / basic_rg / brgUntrusted.ml
index 88edd46d8dee15f0a559da19014ac33653fdd6e6..87a3f60cfff3942573016435c7466cc5597235f2 100644 (file)
@@ -22,29 +22,29 @@ module BV = BrgValidity
 
 (* to share *)
 let type_check err f st = function
-   | a, uri, E.Abst (n, t) ->
+   | ra, na, uri, E.Abst 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
+         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
-   | a, uri, E.Abbr t      ->
+   | ra, na, 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
-           | _        -> B.Cast ([], tt, xt)
+           | _        -> B.Cast (E.empty_node, tt, xt)
         in
-         let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e
+         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
-   | _, _, E.Void          -> assert false
+   | _, _, _, E.Void       -> assert false
 
 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
+      | _, _, uri, E.Abst t -> uri, t
+      | _, _, 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