-let rec xlate_bk_term f = function
- | Z.Sort (a, l) -> f (D.TSort (a, l))
- | Z.GRef (a, n) -> f (D.TGRef (a, n))
- | Z.LRef (a, i) -> f (D.TLRef (a, i, 0))
- | Z.Cast (a, u, t) ->
- let f uu tt = f (D.TCast (a, uu, tt)) in
- let f uu = xlate_bk_term (f uu) t in
- xlate_bk_term f u
- | Z.Appl (a, u, t) ->
- let f uu tt = f (D.TAppl (a, [uu], tt)) in
- let f uu = xlate_bk_term (f uu) t in
- xlate_bk_term f u
- | Z.Bind (a, b, t) ->
- let f bb tt = f (D.TBind (a, bb, tt)) in
- let f bb = xlate_bk_term (f bb) t in
- xlate_bk_bind f b
+let rec xlate_bk_term f c = function
+ | Z.Sort h -> f (D.TSort ([], h))
+ | Z.GRef s -> f (D.TGRef ([], s))
+ | Z.LRef l ->
+ let f i = f (D.TLRef ([], i, 0)) in
+ Z.nth C.err f l c
+ | Z.Cast (u, t) ->
+ let f tt uu = f (D.TCast ([], uu, tt)) in
+ let f tt = xlate_bk_term (f tt) c u in
+ xlate_bk_term f c t
+ | Z.Appl (u, t) ->
+ let f tt uu = f (D.TAppl ([], [uu], tt)) in
+ let f tt = xlate_bk_term (f tt) c u in
+ xlate_bk_term f c t
+ | Z.Bind (a, l, b, t) ->
+ let f tt bb = f (D.TBind (a, bb, tt)) in
+ let f tt = xlate_bk_bind (f tt) c b in
+ let cc = Z.push "xlate_bk_term" C.start c a l b in
+ xlate_bk_term f cc t