From 105236d275296be7ab2561f83ec539a1d166b445 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 May 2009 21:46:42 +0000 Subject: [PATCH] ppsubst commented out in ppobj --- helm/software/components/ng_kernel/nCicPp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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, _) -> -- 2.39.2