"axiom " ^ name ^ " : " ^
ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
| (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
"axiom " ^ name ^ " : " ^
ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
| (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->