- | LRef_ (_, Some w) -> ho_whd f c m w
- | GRef_ (_, _, _, E.Abst w) -> ho_whd f c m w
- | GRef_ (_, _, _, E.Abbr v) -> ho_whd f c m v
- | LRef_ (_, None) -> assert false
- | GRef_ (_, _, _, E.Void) -> assert false
+ | LRef_ (_, Some w) -> ho_whd f c m w
+ | GRef_ (_, _, _, E.Abst (_, w)) -> ho_whd f c m w
+ | GRef_ (_, _, _, E.Abbr (_, v)) -> ho_whd f c m v
+ | LRef_ (_, None) -> assert false
+ | GRef_ (_, _, _, E.Void) -> assert false