Added some "\n" here and there to the pretty-printing of Match.

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 2c46fef6f18a75874ff5486c71f2e107a96528ec..57a3752fe7b99901845aa6a144417921cee07774 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -23,8 +23,8 @@ let trivial_pp_term ~context ~subst ~metasenv =
    | C.LetIn (name,ty,t,b) -> 
       "(let "^name^":"^aux ctx ty^":="^aux ctx t^" in "^aux (name::ctx) b^")"
    | C.Match (_,oty,t,pl) ->
-      " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ "[" ^
-      String.concat "|" (List.map (aux ctx) pl) ^ "]"
+      " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ " with\n" ^ "[" ^
+      String.concat "\n|" (List.map (aux ctx) pl) ^ "]\n"
    | C.Appl l -> "("^String.concat " " (List.map (aux ctx) l) ^")"
    | C.Implicit _ -> "?"
    | C.Meta (n,_) -> "?"^string_of_int n