From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 9 Apr 2008 12:20:22 +0000 (+0000)
Subject: Added some "\n" here and there to the pretty-printing of Match.
X-Git-Tag: make_still_working~5381
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=beac0e2f104073b8a037c4259134ad8cfb441d29;p=helm.git

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 2c46fef6f..57a3752fe 100644
--- 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