let rec icm a = function
| B.Sort _
| B.LRef _
- | B.GRef _ -> succ a
- | B.Bind (_, B.Void, t) -> icm (succ a) t
- | B.Cast (_, u, t) -> icm (icm a u) t
+ | B.GRef _ -> succ a
+ | B.Bind (_, B.Void, t) -> icm (succ a) t
+ | B.Cast (_, u, t) -> icm (icm a u) t
| B.Appl (_, u, t)
- | B.Bind (_, B.Abst (_, u), t)
- | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
+ | B.Bind (_, B.Abst (_, _, u), t)
+ | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
let iter map d =
let rec iter_bind d = function
- | B.Void -> B.Void
- | B.Abst (n, w) -> B.Abst (n, iter_term d w)
- | B.Abbr v -> B.Abbr (iter_term d v)
+ | B.Void -> B.Void
+ | B.Abst (x, n, w) -> B.Abst (x, n, iter_term d w)
+ | B.Abbr v -> B.Abbr (iter_term d v)
and iter_term d = function
| B.Sort _ as t -> t
| B.GRef _ as t -> t