Cic.term * Cic.substitution * Cic.metasenv
(** {2 Pretty printers} *)
+val use_low_level_ppterm_in_context : bool ref
+val set_ppterm_in_context :
+ (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context ->
+ string) -> unit
val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string
val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string