]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/nCicPp.mli
debugging started
[helm.git] / helm / software / components / ng_kernel / nCicPp.mli
1 val set_ppterm: 
2   (context:NCic.context -> 
3    subst:NCic.substitution -> 
4    metasenv:NCic.metasenv ->
5     NCic.term -> string) -> unit
6
7 val ppterm: 
8   ?context:NCic.context -> 
9   ?subst:NCic.substitution -> 
10   ?metasenv:NCic.metasenv ->
11    NCic.term -> string
12
13 val trivial_pp_term: 
14    context:NCic.context -> 
15    subst:NCic.substitution -> 
16    metasenv:NCic.metasenv ->
17     NCic.term -> string