module G = Options
module B = Brg
+IFDEF TYPE THEN
+
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.Appl (_, _, u, 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.Abst (r, n, w) -> B.Abst (r, 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
+ | B.Sort _ as t -> t
+ | B.GRef _ as t -> t
| B.LRef (a, i) as t -> if i < d then t else map d a i
- | B.Cast (a, w, v) -> B.Cast (a, iter_term d w, iter_term d v)
- | B.Appl (a, x, w, u) -> B.Appl (a, x, iter_term d w, iter_term d u)
- | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
+ | B.Cast (w, v) -> B.Cast (iter_term d w, iter_term d v)
+ | B.Appl (a, w, u) -> B.Appl (a, iter_term d w, iter_term d u)
+ | B.Bind (y, b, u) -> B.Bind (y, iter_bind d b, iter_term (succ d) u)
in
iter_term d
*)
iter (lift_map h) d t
end
+
+END