-let ppterm t = "TODO";;
+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
+;;