-let push_abst f a w lenv =
- let bw = D.Abst (false, N.infinite, w) in
- D.push_bind f a bw lenv
-
-let add_proj e t = match e with
- | D.ESort -> t
- | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t)
- | _ -> D.TProj (E.empty_node, e, t)
+let push_abst f y w lenv =
+ let bw = D.Abst (false, N.infinity, w) in
+ D.push_bind f E.empty_node y 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, x, v) -> set_name_y (D.push_appl f x 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, _, y, b) -> D.TBind (E.compose y yt, b, t)
+ | e ->
+ D.TProj (D.set_attrs C.start yt e, t)