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

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

val ppcontext:
  subst:NCic.substitution -> 
  metasenv:NCic.metasenv ->
  NCic.context -> string 

val trivial_pp_term: 
   context:NCic.context -> 
   subst:NCic.substitution -> 
   metasenv:NCic.metasenv ->
   ?inside_fix:bool ->
    NCic.term -> string

val ppobj: NCic.obj -> string