]> 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 c27ec5ed1d94e1c8f0f51fa6f4db44009b798cc8..dc1a310f9d595e67161838a446e6069c667fb120 100644 (file)
@@ -16,16 +16,20 @@ module Z  = Bag
 module ZE = BagEnvironment
 module ZT = BagType
 
+IFDEF TYPE THEN
+
 (* Interface functions ******************************************************)
 
 (* to share *)
 let type_check err f st = function
-   | a, uri, E.Abst (n, 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) (a, uri, E.Abst (n, 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
-   | a, 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) (a, 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