-let push_abst f lenv a w =
- let bw = D.Abst (N.infinite, [w]) in
- let f lenv = f lenv in
- D.push_bind f lenv a bw
-
-let lenv_of_cnt (a, ws) =
- D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws))
+let push_abst f a w lenv =
+ let bw = D.Abst (false, N.infinity, w) in
+ D.push_bind f E.empty_node a bw lenv
+(*
+let rec set_name_y f = function
+ | D.ESort -> f D.ESort
+ | D.EBind (e, a, y, b) -> set_name_y (D.push_bind f a {y with E.b_name = Some ("Y", true)} b) e
+ | D.EAppl (e, a, v) -> set_name_y (D.push_appl f a v) e
+ | D.EProj (e, d) -> let f d = set_name_y (D.push_proj f d) e in set_name_y f d
+*)
+let add_proj yt e t = match e with
+ | D.ESort -> t
+ | D.EBind (D.ESort, _, a, b) -> D.TBind (E.compose a yt, b, t)
+ | e ->
+ D.TProj (D.set_attrs C.start yt e, t)