ppsubst commented out in ppobj

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 27590ed3eed7ff1179eb9ec81006961b09b13eb0..bd5b7f206a4bd1f02404249e5d85d7f35430cbfe 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -244,7 +244,7 @@ let ppobj ~formatter (u,_,metasenv, subst, o) =
   ppmetasenv ~formatter ~subst metasenv;
   F.fprintf formatter "\n";
   F.fprintf formatter "subst:\n";
-  (*ppsubst subst ~formatter ~metasenv;*)
+  (*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "...";
   F.fprintf formatter "\n";
   match o with 
   | NCic.Fixpoint (b, fl, _) ->