X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=a86bc471a06f3a2f3a97b3b0082c965dd0ce8d12;hb=1f974ca07c502d85c9a3760aaaf633bae3c84fb6;hp=c097eacf281869b9ff532d8e127ec80ac5d75d82;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git

diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml
index c097eacf2..a86bc471a 100644
--- a/helm/software/components/cic_unification/cicMetaSubst.ml
+++ b/helm/software/components/cic_unification/cicMetaSubst.ml
@@ -305,6 +305,17 @@ let ppterm_in_context ~metasenv subst term context =
  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