(* $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 ->
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