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
val ppcontext:
metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context ->
string
-val ppterm_in_name_context:
- metasenv:Cic.metasenv -> Cic.substitution -> Cic.term ->
- (Cic.name option) list -> string
val ppterm_in_context:
metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string
val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string