V_______________________________________________________________ *)
module B = Brg
+(* module O = Output *)
+
+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.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
if i + h >= 0 then B.LRef (a, i + h) else assert false
let lift h d t =
- if h = 0 then t else iter (lift_map h) d t
+ if h = 0 then t else begin
+(* O.icm := succ (* icm *) !O.icm (*t*); *) iter (lift_map h) d t
+ end