X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=1654cdfb21978e3b826d1e6b4b2c69a107606d30;hb=1ef41da37d7b39da1521f53d3b22981556bfbe68;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..1654cdfb2 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1 +1,26 @@
-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:
+  subst:NCic.substitution -> 
+  metasenv:NCic.metasenv ->
+  NCic.context -> string 
+
+val ppobj: NCic.obj -> string