- | 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
+ | LRef_ (_, Some w) -> ho_whd f c m w
+ | GRef_ (_, _, B.Abst w) -> 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