]> matita.cs.unibo.it Git - helm.git/commitdiff
better ppcontext
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Oct 2009 10:14:50 +0000 (10:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Oct 2009 10:14:50 +0000 (10:14 +0000)
helm/software/components/ng_kernel/nCicPp.ml

index fd9932d9fda963233e11f7a78bfdbf48187dec13..1058a48cca4a0faaa09ee2609d4f10a9dc522b08 100644 (file)
@@ -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;