| (name, NCic.Def (bo,ty)) :: tl->
ppcontext ~formatter ~sep ~subst ~metasenv tl;
F.fprintf formatter "%s: " name;
ppterm ~formatter ~subst ~metasenv ~context:tl ty;
F.fprintf formatter " := ";
ppterm ~formatter ~subst ~metasenv ~context:tl bo;
| (name, NCic.Def (bo,ty)) :: tl->
ppcontext ~formatter ~sep ~subst ~metasenv tl;
F.fprintf formatter "%s: " name;
ppterm ~formatter ~subst ~metasenv ~context:tl ty;
F.fprintf formatter " := ";
ppterm ~formatter ~subst ~metasenv ~context:tl bo;