X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=a01895678c0535b655ac4a3c7026d58cc616dd3d;hb=e97c74e4d17e6fc0ce7c39b092f3214244ae21d1;hp=e8b7c6dab465f6c4c6107d4b7050de7607661471;hpb=780525c2f318cfe782c3d41b70607ba9d72bcc80;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index e8b7c6dab..a01895678 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -12,6 +12,9 @@
 (* $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 ppterm: 
   context:NCic.context -> 
@@ -30,6 +33,38 @@ val ppcontext:
 val ppmetasenv:
   subst:NCic.substitution -> NCic.metasenv -> string
 
-val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string
+val ppsubst:
+ metasenv:NCic.metasenv -> ?use_subst:bool -> NCic.substitution -> string
 
 val ppobj: NCic.obj -> string
+
+(* variants that use a formatter 
+module Format : sig
+  val ppterm: 
+    formatter:Format.formatter ->
+    context:NCic.context -> 
+    subst:NCic.substitution -> 
+    metasenv:NCic.metasenv ->
+    ?margin:int ->
+    ?inside_fix:bool ->
+     NCic.term -> unit
+  
+  val ppcontext:
+    ?sep:string ->
+    formatter:Format.formatter ->
+    subst:NCic.substitution -> 
+    metasenv:NCic.metasenv ->
+    NCic.context -> unit 
+  
+  val ppmetasenv:
+    formatter:Format.formatter ->
+    subst:NCic.substitution -> NCic.metasenv -> unit
+  
+  val ppsubst: 
+    formatter:Format.formatter ->
+    metasenv:NCic.metasenv -> NCic.substitution -> unit
+  
+  val ppobj: 
+    formatter:Format.formatter -> NCic.obj -> unit
+end
+*)