]> matita.cs.unibo.it Git - helm.git/blob - components/ng_kernel/nCicPp.mli
tagged 0.5.0-rc1
[helm.git] / components / ng_kernel / nCicPp.mli
1 val set_ppterm: 
2   (context:NCic.context -> 
3    subst:NCic.substitution -> 
4    metasenv:NCic.metasenv ->
5    ?inside_fix:bool ->
6     NCic.term -> string) -> unit
7
8 val ppterm: 
9   context:NCic.context -> 
10   subst:NCic.substitution -> 
11   metasenv:NCic.metasenv ->
12   ?inside_fix:bool ->
13    NCic.term -> string
14
15 val ppcontext:
16   subst:NCic.substitution -> 
17   metasenv:NCic.metasenv ->
18   NCic.context -> string 
19
20 val trivial_pp_term: 
21    context:NCic.context -> 
22    subst:NCic.substitution -> 
23    metasenv:NCic.metasenv ->
24    ?inside_fix:bool ->
25     NCic.term -> string
26
27 val ppobj: NCic.obj -> string