X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=6f9a70d50de2a4a44427882445d1d6433766c181;hb=00676a80c190c829a85be5545a7cafe16384098f;hp=a792e865d060dfdca75eda3b28b01d09427e1930;hpb=613bc202d0810f4386b393bfb369c62dfc78c68c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index a792e865d..6f9a70d50 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -1 +1,9 @@
-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
+;;