X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=96a141ff77e1731fbf52ea33fcea8823f43a56b4;hb=9dac09ff867a3ec6298c85df95579b199da54d27;hp=7a88824c049d8792cce99d2944f2ede4583eff44;hpb=00676a80c190c829a85be5545a7cafe16384098f;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 7a88824c0..96a141ff7 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -5,7 +5,15 @@ val set_ppterm:
     NCic.term -> string) -> unit
 
 val ppterm: 
-  ?context:NCic.context -> 
-  ?subst:NCic.substitution -> 
-  ?metasenv:NCic.metasenv ->
+  context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
    NCic.term -> string
+
+val trivial_pp_term: 
+   context:NCic.context -> 
+   subst:NCic.substitution -> 
+   metasenv:NCic.metasenv ->
+    NCic.term -> string
+
+val ppobj: NCic.obj -> string