- | B.Sort h ->
- let f h = f x (B.Sort h) in H.apply f g h
- | B.LRef i ->
- let f = function
- | Some (_, B.Abst w) -> f x w
- | Some (_, B.Abbr (B.Cast (w, v))) -> f x w
- | Some (_, B.Abbr _) -> assert false
- | Some (_, B.Void) ->
- error1 "reference to excluded variable" c x
- | None ->
- error1 "variable not found" c x
- in
- B.get f c i
- | B.GRef uri ->
- let f = function
- | _, _, B.Abst w -> f x w
- | _, _, B.Abbr (B.Cast (w, v)) -> f x w
- | _, _, B.Abbr _ -> assert false
- | _, _, B.Void ->
- error1 "reference to excluded object" c x
- in
- E.get_obj f uri
- | B.Bind (id, B.Abbr v, t) ->
+ | B.Sort (a, h) ->
+ let h = H.apply g 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) ->