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
| GRef_ (_, {E.n_apix = a1}, _, E.Abst _),
GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
- | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1),
- GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) ->
+ | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)),
+ GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) ->
if a1 = a2 then
let f a =
if a then f a else are_convertible f st true c m1 v1 m2 v2
else
if a1 < a2 then whd (aux m1 r1) c m2 v2 else
whd (aux_rev m2 r2) c m1 v1
- | _, GRef_ (_, _, _, E.Abbr v2) ->
+ | _, GRef_ (_, _, _, E.Abbr (_, v2)) ->
whd (aux m1 r1) c m2 v2
- | GRef_ (_, _, _, E.Abbr v1), _ ->
+ | GRef_ (_, _, _, E.Abbr (_, v1)), _ ->
whd (aux_rev m2 r2) c m1 v1
| Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) ->
let l = P.new_mark () in