X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=ccac8dff67e78112bf8b5379082dbfb5826bed65;hb=be2a030746e20744f9a317a31c7053bcfbb6e505;hp=50204fe990d08ed057e4011182ef0fc41a277058;hpb=e48acbc0d00717ce8f12412673ece4e4ee0e9642;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 50204fe99..ccac8dff6 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -11,30 +11,27 @@
 
 (* $Id$ *)
 
-val set_ppterm: 
-  (context:NCic.context -> 
-   subst:NCic.substitution -> 
-   metasenv:NCic.metasenv ->
-   ?inside_fix:bool ->
-    NCic.term -> string) -> unit
+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 trivial_pp_term: 
-   context:NCic.context -> 
-   subst:NCic.substitution -> 
-   metasenv:NCic.metasenv ->
-   ?inside_fix:bool ->
-    NCic.term -> string
+val ppmetasenv:
+  subst:NCic.substitution -> NCic.metasenv -> string
+
+val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string
 
 val ppobj: NCic.obj -> string