]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_ag/bagUntrusted.ml
- new attributes system
[helm.git] / helm / software / helena / src / basic_ag / bagUntrusted.ml
index c27ec5ed1d94e1c8f0f51fa6f4db44009b798cc8..9efbf91824979cdbbd75d3d8a5b8f1d4bb8b27ee 100644 (file)
@@ -20,12 +20,12 @@ module ZT = BagType
 
 (* 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 = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in
+      let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abst xt) in
       ZT.type_of err f st Z.empty_lenv 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 = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in
+      let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abbr xt) in
       ZT.type_of err f st Z.empty_lenv t
-   | _, _, E.Void          -> assert false
+   | _, _, _, E.Void       -> assert false