X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=ccac8dff67e78112bf8b5379082dbfb5826bed65;hb=b378b7f4f2a3a897c4b69f44d4d1d54cc4d0aa56;hp=1654cdfb21978e3b826d1e6b4b2c69a107606d30;hpb=1ef41da37d7b39da1521f53d3b22981556bfbe68;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 1654cdfb2..ccac8dff6 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -11,16 +11,27 @@
 
 (* $Id$ *)
 
+val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
+
+val r2s: bool -> NReference.reference -> string
+
 val ppterm: 
   context:NCic.context -> 
   subst:NCic.substitution -> 
   metasenv:NCic.metasenv ->
+  ?margin:int ->
   ?inside_fix:bool ->
    NCic.term -> string
 
 val ppcontext:
+  ?sep:string ->
   subst:NCic.substitution -> 
   metasenv:NCic.metasenv ->
   NCic.context -> string 
 
+val ppmetasenv:
+  subst:NCic.substitution -> NCic.metasenv -> string
+
+val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string
+
 val ppobj: NCic.obj -> string