]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_ag/bagUntrusted.ml
update in helena
[helm.git] / helm / software / helena / src / basic_ag / bagUntrusted.ml
index 0b5fa7dba30e4d716947e45fb896877bacafe4eb..dc1a310f9d595e67161838a446e6069c667fb120 100644 (file)
@@ -22,14 +22,14 @@ IFDEF TYPE THEN
 
 (* to share *)
 let type_check err f st = function
-   | ra, na, uri, E.Abst t ->
+   | ra, na, uri, E.Abst (a, t) ->
       let err msg = err (L.Uri uri :: msg) in      
-      let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abst xt) in
+      let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.abst a xt) in
       ZT.type_of err f st Z.empty_lenv t
-   | ra, na, uri, E.Abbr t ->
+   | ra, na, uri, E.Abbr (a, t) ->
       let err msg = err (L.Uri uri :: msg) in
-      let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abbr xt) in
+      let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.abbr a xt) in
       ZT.type_of err f st Z.empty_lenv t
-   | _, _, _, E.Void       -> assert false
+   | _, _, _, E.Void            -> assert false
 
 END