| D.TProj (_, e, t) ->
D.shift (xlate_term st f c) e t
(* this case should be removed by improving alpha-conversion *)
- | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
- xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus st n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+ | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) ->
+ xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t)))
| D.TBind (a, b, t) ->
let f cc =
let a, l, b = List.hd cc in
xlate_bind st f c a b
and xlate_bind st f c a = function
- | D.Abst (_, w) ->
+ | D.Abst (_, _, w) ->
let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in
xlate_term st f c w
- | D.Abbr v ->
+ | D.Abbr v ->
let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
xlate_term st f c v
- | D.Void ->
+ | D.Void ->
Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void
(* internal functions: bag to crg term **************************************)
and xlate_bk_bind f c = function
| Z.Abst t ->
- let f tt = f (D.Abst (N.infinite, tt)) in
+ let f tt = f (D.Abst (false, N.infinite, tt)) in
xlate_bk_term f c t
| Z.Abbr t ->
let f tt = f (D.Abbr tt) in