- | B.Sort (a, h) ->
- let f h = f x (B.Sort (a, h)) in H.apply f g h
- | B.LRef (_, i) ->
- let f = function
- | B.Abst (_, w) ->
- S.lift (f x) (succ i) (0) w
- | B.Abbr (_, B.Cast (_, w, _)) ->
- S.lift (f x) (succ i) (0) w
- | B.Abbr _ -> assert false
- | B.Void _ ->
- error1 "reference to excluded variable" m x
- in
- R.get f m i
- | B.GRef (_, uri) ->
- let f = function
- | _, _, 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" m x
- in
- E.get_obj f uri
- | B.Bind (B.Abbr (a, v), t) ->
+ | B.Sort (a, h) ->
+ let h = H.apply h in f x (B.Sort (a, h))
+ | B.LRef (_, i) ->
+ begin match R.get m i with
+ | B.Abst w ->
+ f x (S.lift (succ i) (0) w)
+ | B.Abbr (B.Cast (_, w, _)) ->
+ f x (S.lift (succ i) (0) w)
+ | B.Abbr _ -> assert false
+ | B.Void ->
+ error1 err "reference to excluded variable" m x
+ end
+ | B.GRef (_, uri) ->
+ begin match E.get_entity uri with
+ | _, _, Y.Abst w -> f x w
+ | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
+ | _, _, Y.Abbr _ -> assert false
+ | _, _, Y.Void ->
+ error1 err "reference to unknown entry" m x
+ end
+ | B.Bind (a, B.Abbr v, t) ->