- | _, _, B.Abst, w -> f w
- | _, _, B.Abbr, B.Cast (w, v) -> f w
- | _, _, B.Abbr, _ -> error "gref"
- in
- E.get_obj f uri
- | B.Bind (id, b, u, t) ->
- let f uu tt = match b, t with
- | B.Abst, _
- | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt))
- | _ -> f (B.Bind (id, b, B.Cast (uu, u), tt))
- in
- let f uu cc = type_of (f uu) g cc t in
- let f uu = R.push (f uu) c b u in
+ | _, _, B.Abst w -> f x w
+ | _, _, B.Abbr (B.Cast (_, w, _)) -> f x w
+ | _, _, B.Abbr _ -> assert false
+ | _, _, B.Void ->
+ error1 "reference to excluded object" c x
+ in
+ E.get_obj f uri
+ | B.Bind (a, B.Abbr v, t) ->
+ let f xv xt tt =
+ f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+ in
+ let f xv cc = b_type_of (f xv) g cc t in
+ let f xv = B.push (f xv) c a (B.Abbr xv) in
+ let f xv vv = match xv with
+ | B.Cast _ -> f xv
+ | _ -> f (B.Cast ([], vv, xv))
+ in
+ type_of f g c v
+ | B.Bind (a, B.Abst u, t) ->
+ let f xu xt tt =
+ f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
+ in
+ let f xu cc = b_type_of (f xu) g cc t in
+ let f xu _ = B.push (f xu) c a (B.Abst xu) in