X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=02b6c86423e805e0f4b54fb1cd5acb1c6b64abf3;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=39fe4f2f6ae7b76fbc0e0f20c4270ebe68401ad7;hpb=a4a2345e2efaf4cc64aa4daf40e2bce05a400f12;p=helm.git

diff --git a/matita/components/ng_kernel/nCicPp.mli b/matita/components/ng_kernel/nCicPp.mli
index 39fe4f2f6..02b6c8642 100644
--- a/matita/components/ng_kernel/nCicPp.mli
+++ b/matita/components/ng_kernel/nCicPp.mli
@@ -11,34 +11,13 @@
 
 (* $Id$ *)
 
-val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
-val set_get_obj: (NUri.uri -> NCic.obj) -> unit
-
-val r2s: bool -> NReference.reference -> string
+val r2s: #NCic.status -> bool -> NReference.reference -> string
 
 val string_of_flavour: NCic.def_flavour -> 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 -> ?use_subst:bool -> NCic.substitution -> string
-
-val ppobj: NCic.obj -> string
+(* low-level pretty printer;
+   all methods are meant to be overridden in ApplyTransformation *)
+class status: NCic.cstatus
 
 (* variants that use a formatter 
 module Format : sig