better ppcontext

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 62dc58e4ece81720642de8bd74977029e8f691b9..fd9932d9fda963233e11f7a78bfdbf48187dec13 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -195,20 +195,25 @@ let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
   ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t
 ;;
 
-let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function
+let rec ppcontext ~formatter ?(sep=";") ~subst ~metasenv = function
   | [] -> ()
   | (name, NCic.Decl t) :: tl -> 
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
       F.fprintf formatter "%s: " name;
       ppterm ~formatter ~subst ~metasenv ~context:tl t;
-      F.fprintf formatter "%s" sep
+      F.fprintf formatter "%s@;" sep
   | (name, NCic.Def (bo,ty)) :: tl->
       ppcontext ~formatter ~sep ~subst ~metasenv tl;
       F.fprintf formatter "%s: " name;
       ppterm ~formatter ~subst ~metasenv ~context:tl ty;
       F.fprintf formatter " := ";
       ppterm ~formatter ~subst ~metasenv ~context:tl bo;
-      F.fprintf formatter "%s" sep
+      F.fprintf formatter "%s@;" sep
+;;
+let ppcontext ~formatter ?sep ~subst ~metasenv c =
+  F.fprintf formatter "@[<hov>";
+  ppcontext ~formatter ?sep ~subst ~metasenv c;
+  F.fprintf formatter "@]";
 ;;
 
 let ppmetaattrs =