X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=ef535cee8f38da02309066c78e465533c2f037d6;hb=3ec1830d5251709ed6c4899c74903498a6cd2744;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..ef535cee8 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -9,3 +9,9 @@ val ppterm:
   ?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