in
ppterm_in_name_context ~metasenv subst term name_context
+let ppterm_in_context_ref = ref ppterm_in_context
+let set_ppterm_in_context f =
+ ppterm_in_context_ref := f
+let use_low_level_ppterm_in_context = ref false
+
+let ppterm_in_context ~metasenv subst term context =
+ if !use_low_level_ppterm_in_context then
+ ppterm_in_context ~metasenv subst term context
+ else
+ !ppterm_in_context_ref ~metasenv subst term context
+
let ppcontext' ~metasenv ?(sep = "\n") subst context =
let separate s = if s = "" then "" else s ^ sep in
List.fold_right