let rec ho_whd f c m x =
(* L.warn "entering R.ho_whd"; *)
let aux m = function
- | Sort_ h -> f (Sort h)
- | Bind_ (_, _, w, _) ->
+ | 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_ (_, _, 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
in
whd aux c m x