]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgUntrusted.ml
basic_rg: bugfix in AST to allow attributes in global entries
[helm.git] / helm / software / lambda-delta / basic_rg / brgUntrusted.ml
index f9c23d73fb94c9426539292c0f6497d9f8ef0c9a..67c756b46b512fd8bc69bd84cdd06147416fb9dd 100644 (file)
@@ -19,15 +19,15 @@ module T = BrgType
 
 (* to share *)
 let type_check f ?(si=false) g = function
-   | None                    -> f None None
-   | Some (e, uri, B.Abst t) ->
+   | None                           -> f None None
+   | Some (e, uri, B.Abst (a, t))   ->
       let f tt obj = f (Some tt) (Some obj) in
-      let f xt tt = E.set_obj (f tt) (e, uri, B.Abst xt) in
+      let f xt tt = E.set_obj (f tt) (e, uri, B.abst a xt) in
       L.loc := e; T.type_of f ~si g R.empty_machine t
-   | Some (e, uri, B.Abbr t) ->
+   | Some (e, uri, B.Abbr (a, t))   ->
       let f tt obj = f (Some tt) (Some obj) in
-      let f xt tt = E.set_obj (f tt) (e, uri, B.Abbr xt) in
+      let f xt tt = E.set_obj (f tt) (e, uri, B.abbr a xt) in
       L.loc := e; T.type_of f ~si g R.empty_machine t
-   | Some (e, uri, B.Void)   ->
+   | Some (e, uri, (B.Void _ as b)) ->
       let f obj = f None (Some obj) in
-      L.loc := e; E.set_obj f (e, uri, B.Void)
+      L.loc := e; E.set_obj f (e, uri, b)