+(* lenv/term pretty printing ************************************************)
+
+let name err frm a =
+ let f n = function
+ | true -> F.fprintf frm "%s" n
+ | false -> F.fprintf frm "^%s" n
+ in
+ Y.name err f a
+
+let rec pp_term e frm = function
+ | B.Sort (_, h) ->
+ let err _ = F.fprintf frm "@[*%u@]" h in
+ let f s = F.fprintf frm "@[%s@]" s in
+ H.string_of_sort err f h
+ | B.LRef (_, i) ->
+ let err _ = F.fprintf frm "@[#%u@]" i in
+ if !O.indexes then err () else
+ let _, _, a, b = B.get e i in
+ F.fprintf frm "@[%a@]" (name err) a
+ | B.GRef (_, s) ->
+ F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+ | B.Cast (_, u, t) ->
+ F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t
+ | B.Appl (_, v, t) ->
+ F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t
+ | B.Bind (a, B.Abst w, t) ->
+ let f a =
+ let ee = B.push e B.empty a (B.abst w) in
+ F.fprintf frm "@[[%a:%a].%a@]" (name C.err) a (pp_term e) w (pp_term ee) t
+ in
+ rename f e a
+ | B.Bind (a, B.Abbr v, t) ->
+ let f a =
+ let ee = B.push e B.empty a (B.abbr v) in
+ F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t
+ in
+ rename f e a
+ | B.Bind (a, B.Void, t) ->
+ let f a =
+ let ee = B.push e B.empty a B.Void in
+ F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t
+ in
+ rename f e a
+
+let pp_lenv frm e =
+ let pp_entry f e c a b x = f x (*match b with
+ | B.Abst (a, w) ->
+ let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in
+ rename f x a
+ | B.Abbr (a, v) ->
+ let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in
+ rename f c a
+ | B.Void a ->
+ let f a = F.fprintf frm "@,%a" (name C.err) a; f a in
+ rename f c a
+*) in
+ B.fold_right ignore pp_entry e B.empty