- simpler attribute system

[helm.git] / helm / software / helena / src / basic_ag / bagType.ml

diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml
index 009a2eaf9ec5e08d673881df3b43bdf6156fbc46..1f47b60ddc4a005fac7ebeaff5f5362abaa74c3a 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagType.ml
+++ b/helm/software/helena/src/basic_ag/bagType.ml
@@ -66,33 +66,33 @@ let rec b_type_of err f st c x =
         | _, _, _, E.Void                 -> assert false
       in
       ZE.get_entity f uri   
-   | Z.Bind (a, l, Z.Abbr v, t) ->
+   | Z.Bind (y, l, Z.Abbr v, t) ->
       let f xv xt tt =
-         f (S.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
+         f (S.sh2 v xv t xt x (Z.bind_abbr y l)) (Z.bind_abbr y l xv tt)
       in
       let f xv cc = b_type_of err (f xv) st cc t in
-      let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in
+      let f xv = Z.push "type abbr" (f xv) c y l (Z.Abbr xv) in
       let f xv vv = match xv with 
         | Z.Cast _ -> f xv
          | _        -> f (Z.Cast (vv, xv))
       in
       type_of err f st c v
-   | Z.Bind (a, l, Z.Abst u, t) ->
+   | Z.Bind (y, l, Z.Abst u, t) ->
       let f xu xt tt =
-        f (S.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
+        f (S.sh2 u xu t xt x (Z.bind_abst y l)) (Z.bind_abst y l xu tt)
       in
       let f xu cc = b_type_of err (f xu) st cc t in
-      let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in
+      let f xu _ = Z.push "type abst" (f xu) c y l (Z.Abst xu) in
       type_of err f st c u
-   | Z.Bind (a, l, Z.Void, t)   ->
+   | Z.Bind (y, l, Z.Void, t)   ->
       let f xt tt = 
-         f (S.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
+         f (S.sh1 t xt x (Z.bind y l Z.Void)) (Z.bind y l Z.Void tt)
       in
       let f cc = b_type_of err f st cc t in
-      Z.push "type void" f c a l Z.Void   
+      Z.push "type void" f c y l Z.Void   
    | Z.Appl (v, t)              ->
       let f xv vv xt tt = function
-        | ZR.Abst w                             -> 
+        | ZR.Abst w -> 
            if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
            let f a =                
 (*            L.warn (Printf.sprintf "Convertible: %b" a); *)
@@ -100,7 +100,7 @@ let rec b_type_of err f st c x =
               else error3 err c xv vv w
            in
            ZR.are_convertible f st c w vv
-        | _                                    -> 
+        | _         -> 
            error1 err "not a function" c xt
       in
       let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in