let ppterm = 
  ref (fun ~context ~subst ~metasenv t -> "Please, set a pp callback")
;;

let set_ppterm f = ppterm := f;;

let ppterm ?(context=[]) ?(subst=[]) ?(metasenv=[]) t = 
  !ppterm ~context ~subst ~metasenv t
;;