From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 May 2009 21:46:42 +0000 (+0000)
Subject: ppsubst commented out in ppobj
X-Git-Tag: make_still_working~3991
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=105236d275296be7ab2561f83ec539a1d166b445;p=helm.git

ppsubst commented out in ppobj
---

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 27590ed3e..bd5b7f206 100644
--- 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, _) ->