]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/nCicPp.mli
added mk_fix i j r that given an r of a fix generated another fix on i and j
[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    ?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 trivial_pp_term: 
16    context:NCic.context -> 
17    subst:NCic.substitution -> 
18    metasenv:NCic.metasenv ->
19    ?inside_fix:bool ->
20     NCic.term -> string
21
22 val ppobj: NCic.obj -> string