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=3aa3c027d34d3f91b7876cf90cea0aa0905b0b64;hpb=613bc202d0810f4386b393bfb369c62dfc78c68c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 3aa3c027d..ef535cee8 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1 +1,17 @@
-val ppterm: NCic.term -> string
+val set_ppterm: 
+  (context:NCic.context -> 
+   subst:NCic.substitution -> 
+   metasenv:NCic.metasenv ->
+    NCic.term -> string) -> unit
+
+val ppterm: 
+  ?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