X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicPp.mli;h=50204fe990d08ed057e4011182ef0fc41a277058;hb=283c65c5e52db9bc3ee712358faa6cd6b48d38d0;hp=96a141ff77e1731fbf52ea33fcea8823f43a56b4;hpb=3c8abd24ff28dfd95f1428dae80c5807a328e9ae;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli
index 96a141ff7..50204fe99 100644
--- a/helm/software/components/ng_kernel/nCicPp.mli
+++ b/helm/software/components/ng_kernel/nCicPp.mli
@@ -1,19 +1,40 @@
+(*
+    ||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_ppterm: 
   (context:NCic.context -> 
    subst:NCic.substitution -> 
    metasenv:NCic.metasenv ->
+   ?inside_fix:bool ->
     NCic.term -> string) -> unit
 
 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 trivial_pp_term: 
    context:NCic.context -> 
    subst:NCic.substitution -> 
    metasenv:NCic.metasenv ->
+   ?inside_fix:bool ->
     NCic.term -> string
 
 val ppobj: NCic.obj -> string