From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Oct 2009 10:14:50 +0000 (+0000)
Subject: better ppcontext
X-Git-Tag: make_still_working~3322
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d02e9de60490bc1928ca7d32db2263e21c0148de;p=helm.git

better ppcontext
---

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index fd9932d9f..1058a48cc 100644
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -195,7 +195,7 @@ let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
   ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t
 ;;
 
-let rec ppcontext ~formatter ?(sep=";") ~subst ~metasenv = function
+let rec ppcontext ~formatter ?(sep="; ") ~subst ~metasenv = function
   | [] -> ()
   | (name, NCic.Decl t) :: tl -> 
       ppcontext ~formatter ~sep ~subst ~metasenv tl;