]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicPp.mli
- hExtlib: added debugging information for split_nth
[helm.git] / helm / software / components / ng_kernel / nCicPp.mli
index 1dbdeadc0155df1a08c4eb71a919755e55a94ecc..ccac8dff67e78112bf8b5379082dbfb5826bed65 100644 (file)
@@ -1,27 +1,37 @@
-val set_ppterm: 
-  (context:NCic.context -> 
-   subst:NCic.substitution -> 
-   metasenv:NCic.metasenv ->
-   ?inside_fix:bool ->
-    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 r2s: bool -> NReference.reference -> string
 
 val ppterm: 
   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 trivial_pp_term: 
-   context:NCic.context -> 
-   subst:NCic.substitution -> 
-   metasenv:NCic.metasenv ->
-   ?inside_fix:bool ->
-    NCic.term -> string
+val ppmetasenv:
+  subst:NCic.substitution -> NCic.metasenv -> string
+
+val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string
 
 val ppobj: NCic.obj -> string