val set_ppterm: 
  (context:NCic.context -> 
   subst:NCic.substitution -> 
   metasenv:NCic.metasenv ->
    NCic.term -> string) -> unit

val ppterm: 
  ?context:NCic.context -> 
  ?subst:NCic.substitution -> 
  ?metasenv:NCic.metasenv ->
   NCic.term -> string