let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
let buff = Buffer.create 100 in
let f = Format.formatter_of_buffer buff in
let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
let buff = Buffer.create 100 in
let f = Format.formatter_of_buffer buff in
| C.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
aux ctx (NCicSubstitution.subst_meta lc t)
| C.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
aux ctx (NCicSubstitution.subst_meta lc t)
let rec ppmetasenv ~subst metasenv = function
| [] -> ""
| (i,(name, ctx, ty)) :: tl ->
let rec ppmetasenv ~subst metasenv = function
| [] -> ""
| (i,(name, ctx, ty)) :: tl ->
ppcontext ~sep:"; " ~subst ~metasenv ctx ^
" ⊢ ?"^string_of_int i^name^" : " ^
ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^
ppcontext ~sep:"; " ~subst ~metasenv ctx ^
" ⊢ ?"^string_of_int i^name^" : " ^
ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^