X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=c260e8c61a70c9f1c29f80e9b0f3c6367bb10eea;hb=20427121e8114fa60b64bd1669a0fc734bf39205;hp=7a88824c049d8792cce99d2944f2ede4583eff44;hpb=00676a80c190c829a85be5545a7cafe16384098f;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 7a88824c0..c260e8c61 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1,11 +1,38 @@
-val set_ppterm: 
-  (context:NCic.context -> 
-   subst:NCic.substitution -> 
-   metasenv:NCic.metasenv ->
-    NCic.term -> string) -> unit
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $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 -> 
-  ?subst:NCic.substitution -> 
-  ?metasenv:NCic.metasenv ->
+  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