-(*
-let push2 err f lenv ?attr ?t () = match lenv, attr, t with
- | EBind (e, a, Abst (n, ws)), Some attr, Some t ->
- f (EBind (e, (attr :: a), Abst (n, t :: ws)))
- | EBind (e, a, Abst (n, ws)), None, Some t ->
- f (EBind (e, a, Abst (n, t :: ws)))
- | EBind (e, a, Abbr vs), Some attr, Some t ->
- f (EBind (e, (attr :: a), Abbr (t :: vs)))
- | EBind (e, a, Abbr vs), None, Some t ->
- f (EBind (e, a, Abbr (t :: vs)))
- | EBind (e, a, Void n), Some attr, None ->
- f (EBind (e, (attr :: a), Void (succ n)))
- | EBind (e, a, Void n), None, None ->
- f (EBind (e, a, Void (succ n)))
- | _ -> err ()
-
-let get_index err f i j lenv =
- let rec aux f i k = function
- | ESort -> err i
- | EBind (tl, _, Abst (_, []))
- | EBind (tl, _, Abbr [])
- | EBind (tl, _, Void 0) -> aux f i k tl
- | EBind (_, a, _) when i = 0 ->
- if E.count_names a > j then f (k + j) else err i
- | EBind (tl, a, _) ->
- aux f (pred i) (k + E.count_names a) tl
- | EProj (tl, _, d) -> aux f i k (eshift C.start tl d)
- in
- aux f i 0 lenv
-*)
-let rec names_of_lenv ns = function
- | ESort -> ns
- | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
- | EAppl (tl, _, _) -> names_of_lenv ns tl
- | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
-