From d02e9de60490bc1928ca7d32db2263e21c0148de Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 10:14:50 +0000 Subject: [PATCH] better ppcontext --- 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 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; -- 2.39.2