- | Sort_ h -> f c (Sort h)
- | Bind_ (_, _, w, _) ->
- let f c = f c (Abst w) in unwind_to_context f c m
- | LRef_ (_, Some w) -> ho_whd f c m w
- | GRef_ (_, _, B.Abst u) -> ho_whd f c m u
- | GRef_ (_, _, B.Abbr t) -> ho_whd f c m t
- | LRef_ (_, None) -> assert false
- | GRef_ (_, _, B.Void) -> assert false
+ | Sort_ h -> f (Sort h)
+ | Bind_ (_, _, w, _) ->
+ let f w = f (Abst w) in unwind_to_term f m w
+ | LRef_ (_, Some w) -> ho_whd f c m w
+ | GRef_ (_, uri, B.Abst w) ->
+ let f = function
+ | Abst _ as r -> f r
+ | GRef _ as r -> f r
+ | Sort _ ->
+ let f vs = f (GRef (uri, vs)) in unwind_stack f m
+ in
+ ho_whd f c m w
+ | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v
+ | LRef_ (_, None) -> assert false
+ | GRef_ (_, _, B.Void) -> assert false