X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=507f38d162ded2b801ea873939d3f6bbde82f504;hb=efea8f34e71084fcc6e7791e4927f2f7f8d3f1af;hp=3aa3c027d34d3f91b7876cf90cea0aa0905b0b64;hpb=613bc202d0810f4386b393bfb369c62dfc78c68c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 3aa3c027d..507f38d16 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1 +1,32 @@
-val ppterm: NCic.term -> string
+(*
+    ||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 ppterm: 
+  context:NCic.context -> 
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
+  ?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